Permalink
Browse files

Remove some more "open" and dead code thanks to OCaml4 warnings

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
letouzey
letouzey committed Oct 2, 2012
1 parent 3415801 commit 85c509a0fada387d3af96add3dac6a7c702b5d01
Showing with 34 additions and 1,112 deletions.
  1. +0 −2 grammar/argextend.ml4
  2. +3 −9 grammar/q_constr.ml4
  3. +0 −1 grammar/q_coqast.ml4
  4. +0 −5 grammar/q_util.ml4
  5. +0 −2 grammar/vernacextend.ml4
  6. +1 −36 interp/constrintern.ml
  7. +0 −55 interp/modintern.ml
  8. +0 −2 interp/notation.ml
  9. +0 −1 interp/smartlocate.ml
  10. +1 −13 interp/topconstr.ml
  11. +0 −2 intf/misctypes.mli
  12. +0 −1 kernel/csymtable.ml
  13. +0 −3 kernel/modops.ml
  14. +0 −2 kernel/pre_env.ml
  15. +0 −1 kernel/term.ml
  16. +0 −2 kernel/univ.ml
  17. +0 −12 lib/cList.ml
  18. +0 −1 lib/dyn.ml
  19. +0 −1 lib/gmapl.ml
  20. +0 −5 lib/serialize.ml
  21. +0 −10 lib/store.ml
  22. +0 −2 lib/system.ml
  23. +0 −5 lib/util.ml
  24. +0 −1 lib/xml_parser.ml
  25. +0 −1 library/declaremods.ml
  26. +0 −1 library/dischargedhypsmap.ml
  27. +0 −1 library/global.ml
  28. +0 −1 library/globnames.ml
  29. +0 −2 library/goptions.ml
  30. +0 −2 library/impargs.ml
  31. +2 −11 library/lib.ml
  32. +0 −1 library/libobject.ml
  33. +0 −2 library/library.ml
  34. +2 −2 parsing/egramcoq.ml
  35. +3 −5 parsing/extrawit.ml
  36. +0 −2 parsing/g_ltac.ml4
  37. +0 −11 parsing/g_obligations.ml4
  38. +0 −2 parsing/g_vernac.ml4
  39. +0 −2 parsing/g_xml.ml4
  40. +0 −6 parsing/pcoq.ml4
  41. +0 −2 plugins/cc/ccalgo.ml
  42. +0 −1 plugins/cc/ccproof.ml
  43. +0 −2 plugins/cc/g_congruence.ml4
  44. +0 −1 plugins/decl_mode/decl_mode.ml
  45. +0 −17 plugins/decl_mode/decl_proof_instr.ml
  46. +0 −3 plugins/decl_mode/g_decl_mode.ml4
  47. +0 −1 plugins/decl_mode/ppdecl_proof.ml
  48. +3 −7 plugins/extraction/extract_env.ml
  49. +0 −2 plugins/extraction/g_extraction.ml4
  50. +0 −5 plugins/extraction/haskell.ml
  51. +0 −15 plugins/extraction/mlutil.ml
  52. +0 −2 plugins/extraction/modutil.ml
  53. +0 −3 plugins/firstorder/g_ground.ml4
  54. +0 −4 plugins/firstorder/sequent.ml
  55. +0 −2 plugins/fourier/fourierR.ml
  56. +2 −36 plugins/funind/functional_principles_proofs.ml
  57. +0 −16 plugins/funind/functional_principles_types.ml
  58. +0 −2 plugins/funind/g_indfun.ml4
  59. +0 −38 plugins/funind/glob_term_to_relation.ml
  60. +1 −59 plugins/funind/indfun.ml
  61. +0 −13 plugins/funind/indfun_common.ml
  62. +0 −11 plugins/funind/merge.ml
  63. +0 −16 plugins/funind/recdef.ml
  64. +1 −3 plugins/micromega/certificate.ml
  65. +0 −3 plugins/micromega/g_micromega.ml4
  66. +0 −21 plugins/nsatz/nsatz.ml4
  67. +1 −2 plugins/nsatz/polynom.ml
  68. +0 −12 plugins/omega/coq_omega.ml
  69. +0 −2 plugins/omega/omega.ml
  70. +0 −1 plugins/quote/g_quote.ml4
  71. +0 −3 plugins/quote/quote.ml
  72. +0 −1 plugins/romega/const_omega.ml
  73. +0 −1 plugins/romega/refl_omega.ml
  74. +0 −10 plugins/rtauto/proof_search.ml
  75. +0 −9 plugins/rtauto/refl_tauto.ml
  76. +0 −16 plugins/setoid_ring/newring.ml4
  77. +0 −4 plugins/syntax/ascii_syntax.ml
  78. +0 −2 plugins/syntax/nat_syntax.ml
  79. +0 −1 plugins/syntax/numbers_syntax.ml
  80. +0 −6 plugins/syntax/r_syntax.ml
  81. +0 −7 plugins/syntax/string_syntax.ml
  82. +0 −2 plugins/xml/doubleTypeInference.ml
  83. +0 −3 plugins/xml/dumptree.ml4
  84. +0 −95 plugins/xml/xmlcommand.ml
  85. +1 −7 plugins/xml/xmlentries.ml4
  86. +0 −35 pretyping/cases.ml
  87. +1 −4 pretyping/classops.ml
  88. +0 −4 pretyping/evarconv.ml
  89. +0 −13 pretyping/evarutil.ml
  90. +0 −4 pretyping/evd.ml
  91. +0 −9 pretyping/pretyping.ml
  92. +0 −9 pretyping/program.ml
  93. +0 −2 pretyping/reductionops.ml
  94. +2 −2 pretyping/tacred.ml
  95. +0 −11 pretyping/term_dnet.ml
  96. +0 −6 pretyping/typeclasses.ml
  97. +0 −1 pretyping/typeclasses_errors.ml
  98. +0 −3 pretyping/unification.ml
  99. +0 −3 printing/ppconstr.ml
  100. +0 −2 printing/pptactic.ml
  101. +0 −1 printing/printer.ml
  102. +0 −2 printing/tactic_printer.ml
  103. +5 −7 printing/tactic_printer.mli
  104. +0 −18 proofs/logic.ml
  105. +0 −4 proofs/logic.mli
  106. +1 −5 proofs/pfedit.ml
  107. +0 −2 proofs/proof.ml
  108. +0 −2 proofs/proof_global.ml
  109. +0 −1 proofs/proof_type.ml
  110. +2 −2 proofs/proofview.ml
  111. +0 −19 proofs/refiner.ml
  112. +0 −2 proofs/tacmach.ml
  113. +0 −35 tactics/auto.ml
  114. +0 −6 tactics/autorewrite.ml
  115. +0 −14 tactics/class_tactics.ml4
  116. +0 −7 tactics/eauto.ml4
  117. +0 −16 tactics/elimschemes.ml
  118. +0 −3 tactics/eqdecide.ml4
  119. +0 −2 tactics/equality.ml
  120. +0 −4 tactics/extraargs.ml4
  121. +0 −9 tactics/extratactics.ml4
  122. +0 −1 tactics/hiddentac.ml
  123. +0 −15 tactics/hipattern.ml4
  124. +0 −1 tactics/inv.ml
  125. +0 −13 tactics/nbtermdn.ml
  126. +0 −13 tactics/rewrite.ml4
  127. +0 −22 tactics/tacinterp.ml
  128. +1 −0 tactics/tacticals.mli
  129. +0 −5 tactics/tactics.ml
  130. +0 −2 tactics/tauto.ml4
  131. +0 −1 toplevel/cerrors.ml
  132. +0 −3 toplevel/class.ml
  133. +0 −6 toplevel/classes.ml
  134. +0 −24 toplevel/command.ml
  135. +0 −2 toplevel/mltop.ml4
  136. +1 −22 toplevel/obligations.ml
  137. +0 −7 toplevel/record.ml
  138. +0 −5 toplevel/search.ml
  139. +0 −1 toplevel/vernacinterp.ml
  140. +0 −5 toplevel/whelp.ml4
View
@@ -11,7 +11,6 @@
open Genarg
open Q_util
open Egramml
-open Pcoq
open Compat
let loc = Loc.ghost
@@ -264,7 +263,6 @@ let declare_vernac_argument loc s pr cl =
($wit$, fun _ _ _ _ -> Errors.anomaly "vernac argument needs not wit printer") }
>> ]
-open Vernacexpr
open Pcoq
open Pcaml
open PcamlSig
View
@@ -8,16 +8,10 @@
(*i camlp4deps: "tools/compat5b.cmo" i*)
-open Glob_term
-open Term
-open Names
-open Pattern
open Q_util
-open Pp
open Compat
open Pcaml
open PcamlSig
-open Misctypes
let loc = Loc.ghost
let dloc = <:expr< Loc.ghost >>
@@ -34,9 +28,9 @@ EXTEND
<:expr< snd (Patternops.pattern_of_glob_constr $c$) >> ] ]
;
sort:
- [ [ "Set" -> GSet
- | "Prop" -> GProp
- | "Type" -> GType None ] ]
+ [ [ "Set" -> Misctypes.GSet
+ | "Prop" -> Misctypes.GProp
+ | "Type" -> Misctypes.GType None ] ]
;
ident:
[ [ s = string -> <:expr< Names.id_of_string $str:s$ >> ] ]
View
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pp
open Names
open Q_util
open Compat
View
@@ -8,9 +8,7 @@
(* This file defines standard combinators to build ml expressions *)
-open Extrawit
open Compat
-open Pp
let mlexpr_of_list f l =
List.fold_right
@@ -51,9 +49,6 @@ let mlexpr_of_option f = function
| None -> <:expr< None >>
| Some e -> <:expr< Some $f e$ >>
-open Vernacexpr
-open Genarg
-
let rec mlexpr_of_prod_entry_key = function
| Pcoq.Alist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key s$ >>
| Pcoq.Alist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >>
View
@@ -10,9 +10,7 @@
open Pp
open Util
-open Genarg
open Q_util
-open Q_coqast
open Argextend
open Tacextend
open Pcoq
View
@@ -110,24 +110,18 @@ let global_reference_in_absolute_module dir id =
type internalization_error =
| VariableCapture of identifier * identifier
- | WrongExplicitImplicit
| IllegalMetavariable
| NotAConstructor of reference
| UnboundFixName of bool * identifier
| NonLinearPattern of identifier
| BadPatternsNumber of int * int
- | BadExplicitationNumber of explicitation * int option
exception InternalizationError of Loc.t * internalization_error
let explain_variable_capture id id' =
pr_id id ++ str " is dependent in the type of " ++ pr_id id' ++
strbrk ": cannot interpret both of them with the same type"
-let explain_wrong_explicit_implicit =
- str "Found an explicitly given implicit argument but was expecting" ++
- fnl () ++ str "a regular one"
-
let explain_illegal_metavariable =
str "Metavariables allowed only in patterns"
@@ -146,32 +140,15 @@ let explain_bad_patterns_number n1 n2 =
str "Expecting " ++ int n1 ++ str (plural n1 " pattern") ++
str " but found " ++ int n2
-let explain_bad_explicitation_number n po =
- match n with
- | ExplByPos (n,_id) ->
- let s = match po with
- | None -> str "a regular argument"
- | Some p -> int p in
- str "Bad explicitation number: found " ++ int n ++
- str" but was expecting " ++ s
- | ExplByName id ->
- let s = match po with
- | None -> str "a regular argument"
- | Some p -> (*pr_id (name_of_position p) in*) failwith "" in
- str "Bad explicitation name: found " ++ pr_id id ++
- str" but was expecting " ++ s
-
let explain_internalization_error e =
let pp = match e with
| VariableCapture (id,id') -> explain_variable_capture id id'
- | WrongExplicitImplicit -> explain_wrong_explicit_implicit
| IllegalMetavariable -> explain_illegal_metavariable
| NotAConstructor ref -> explain_not_a_constructor ref
| UnboundFixName (iscofix,id) -> explain_unbound_fix_name iscofix id
| NonLinearPattern id -> explain_non_linear_pattern id
| BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2
- | BadExplicitationNumber (n,po) -> explain_bad_explicitation_number n po in
- pp ++ str "."
+ in pp ++ str "."
let error_bad_inductive_type loc =
user_err_loc (loc,"",str
@@ -283,10 +260,6 @@ let error_inconsistent_scope loc id scopes1 scopes2 =
pr_scope_stack scopes2 ++ strbrk " while it was elsewhere used in " ++
pr_scope_stack scopes1)
-let error_expect_constr_notation_type loc id =
- user_err_loc (loc,"",
- pr_id id ++ str " is bound in the notation to a term variable.")
-
let error_expect_binder_notation_type loc id =
user_err_loc (loc,"",
pr_id id ++
@@ -786,12 +759,6 @@ let product_of_cases_patterns ids idspl =
List.map (fun (subst',ptail) -> (subst@subst',p::ptail)) ptaill) pl)))
idspl (ids,[[],[]])
-let simple_product_of_cases_patterns pl =
- List.fold_right (fun pl ptaill ->
- List.flatten (List.map (fun (subst,p) ->
- List.map (fun (subst',ptail) -> (subst@subst',p::ptail)) ptaill) pl))
- pl [[],[]]
-
(* @return the first variable that occurs twice in a pattern
naive n2 algo *)
@@ -1769,8 +1736,6 @@ open Environ
let my_intern_constr sigma env lvar acc c =
internalize sigma env acc false lvar c
-let my_intern_type sigma env lvar acc c = my_intern_constr sigma env lvar (set_type_scope acc) c
-
let intern_context global_level sigma env impl_env params =
try
let lvar = (([],[]), []) in
View
@@ -6,9 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
-open Util
-open Names
open Entries
open Libnames
open Constrexpr
@@ -28,8 +25,6 @@ val error_not_a_functor : module_struct_entry -> 'a
val error_not_equal : module_path -> module_path -> 'a
-val error_result_must_be_signature : unit -> 'a
-
oval error_not_a_modtype_loc : loc -> string -> 'a
val error_not_a_module_loc : loc -> string -> 'a
@@ -41,9 +36,6 @@ val error_with_in_module : unit -> 'a
val error_application_to_module_type : unit -> 'a
*)
-let error_result_must_be_signature () =
- error "The result module type must be a signature."
-
let error_not_a_modtype_loc loc s =
Loc.raise loc (Modops.ModuleTypingError (Modops.NotAModuleType s))
@@ -60,53 +52,6 @@ let error_application_to_module_type loc =
Loc.raise loc (ModuleInternalizationError IncorrectModuleApplication)
-
-
-let rec make_mp mp = function
- [] -> mp
- | h::tl -> make_mp (MPdot(mp, label_of_id h)) tl
-
-(*
-(* Since module components are not put in the nametab we try to locate
-the module prefix *)
-exception BadRef
-
-let lookup_qualid (modtype:bool) qid =
- let rec make_mp mp = function
- [] -> mp
- | h::tl -> make_mp (MPdot(mp, label_of_id h)) tl
- in
- let rec find_module_prefix dir n =
- if n<0 then raise Not_found;
- let dir',dir'' = List.chop n dir in
- let id',dir''' =
- match dir'' with
- | hd::tl -> hd,tl
- | _ -> anomaly "This list should not be empty!"
- in
- let qid' = make_qualid dir' id' in
- try
- match Nametab.locate qid' with
- | ModRef mp -> mp,dir'''
- | _ -> raise BadRef
- with
- Not_found -> find_module_prefix dir (pred n)
- in
- try Nametab.locate qid
- with Not_found ->
- let (dir,id) = repr_qualid qid in
- let pref_mp,dir' = find_module_prefix dir (List.length dir - 1) in
- let mp =
- List.fold_left (fun mp id -> MPdot (mp, label_of_id id)) pref_mp dir'
- in
- if modtype then
- ModTypeRef (make_ln mp (label_of_id id))
- else
- ModRef (MPdot (mp,label_of_id id))
-
-*)
-
-
(* Search for the head of [qid] in [binders].
If found, returns the module_path/kernel_name created from the dirpath
and the basename. Searches Nametab otherwise.
View
@@ -399,8 +399,6 @@ let interp_notation loc ntn local_scopes =
user_err_loc
(loc,"",str ("Unknown interpretation for notation \""^ntn^"\"."))
-let isGApp = function GApp _ -> true | _ -> false
-
let uninterp_notations c =
List.map_append (fun key -> Gmapl.find key !notations_key_table)
(glob_constr_keys c)
View
@@ -14,7 +14,6 @@
(* *)
open Pp
open Errors
-open Util
open Libnames
open Globnames
open Misctypes
View
@@ -20,7 +20,7 @@ open Constrexpr_ops
let oldfashion_patterns = ref (true)
-let write_oldfashion_patterns = Goptions.declare_bool_option {
+let _ = Goptions.declare_bool_option {
Goptions.optsync = true; Goptions.optdepr = false;
Goptions.optname =
"Constructors in patterns require all their arguments but no parameters instead of explicit parameters and arguments";
@@ -244,18 +244,6 @@ let rec replace_vars_constr_expr l = function
| c -> map_constr_expr_with_binders List.remove_assoc
replace_vars_constr_expr l c
-(**********************************************************************)
-(* Concrete syntax for modules and modules types *)
-
-type with_declaration_ast =
- | CWith_Module of identifier list Loc.located * qualid Loc.located
- | CWith_Definition of identifier list Loc.located * constr_expr
-
-type module_ast =
- | CMident of qualid Loc.located
- | CMapply of Loc.t * module_ast * module_ast
- | CMwith of Loc.t * module_ast * with_declaration_ast
-
(* Returns the ranges of locs of the notation that are not occupied by args *)
(* and which are then occupied by proper symbols of the notation (or spaces) *)
View
@@ -7,7 +7,6 @@
(************************************************************************)
open Names
-open Libnames
(** Basic types used both in [constr_expr] and in [glob_constr] *)
@@ -60,7 +59,6 @@ type 'a cast_type =
| CastVM of 'a
| CastCoerce (** Cast to a base type (eg, an underlying inductive type) *)
-
(** Bindings *)
type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
View
@@ -94,7 +94,6 @@ let annot_tbl = Hashtbl.create 31
exception NotEvaluated
-open Pp
let key rk =
match !rk with
| Some k -> (*Pp.msgnl (str"found at: "++int k);*) k
View
@@ -98,9 +98,6 @@ let error_no_module_to_end _ =
let error_no_modtype_to_end _ =
raise (ModuleTypingError NoModuleTypeToEnd)
-let error_not_a_modtype s =
- raise (ModuleTypingError (NotAModuleType s))
-
let error_not_a_module s =
raise (ModuleTypingError (NotAModule s))
View
@@ -106,8 +106,6 @@ let push_named_context_val d (ctxt,vals) =
let rval = ref VKnone in
Sign.add_named_decl d ctxt, (id,rval)::vals
-exception ASSERT of rel_context
-
let push_named d env =
(* if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context);
assert (env.env_rel_context = []); *)
View
@@ -828,7 +828,6 @@ let subst1 lam = substl [lam]
let substnl_decl laml k = map_rel_declaration (substnl laml k)
let substl_decl laml = substnl_decl laml 0
let subst1_decl lam = substl_decl [lam]
-let substnl_named laml k = map_named_declaration (substnl laml k)
let substl_named_decl = substl_decl
let subst1_named_decl = subst1_decl
View
@@ -29,8 +29,6 @@ open Util
union-find algorithm. The assertions $<$ and $\le$ are represented by
adjacency lists *)
-let compare_ints (x:int) (y:int) = Pervasives.compare x y
-
module UniverseLevel = struct
type t =
View
@@ -550,13 +550,6 @@ let rec sep_last = function
| hd::[] -> (hd,[])
| hd::tl -> let (l,tl) = sep_last tl in (l,hd::tl)
-let try_find_i f =
- let rec try_find_f n = function
- | [] -> failwith "try_find_i"
- | h::t -> try f n h with Failure _ -> try_find_f (n+1) t
- in
- try_find_f
-
let rec find_map f = function
| [] -> raise Not_found
| x :: l ->
@@ -670,11 +663,6 @@ let rec split3 = function
| (x,y,z)::l ->
let (rx, ry, rz) = split3 l in (x::rx, y::ry, z::rz)
-let rec insert_in_class f a = function
- | [] -> [[a]]
- | (b::_ as l)::classes when f a b -> (a::l)::classes
- | l::classes -> l :: insert_in_class f a classes
-
let firstn n l =
let rec aux acc = function
| (0, l) -> List.rev acc
View
@@ -7,7 +7,6 @@
(************************************************************************)
open Errors
-open Util
(* Dynamics, programmed with DANGER !!! *)
Oops, something went wrong.

0 comments on commit 85c509a

Please sign in to comment.