Skip to content
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...
1 parent 3415801 commit 85c509a0fada387d3af96add3dac6a7c702b5d01 letouzey committed
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
2 grammar/argextend.ml4
@@ -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
12 grammar/q_constr.ml4
@@ -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
1 grammar/q_coqast.ml4
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pp
open Names
open Q_util
open Compat
View
5 grammar/q_util.ml4
@@ -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
2 grammar/vernacextend.ml4
@@ -10,9 +10,7 @@
open Pp
open Util
-open Genarg
open Q_util
-open Q_coqast
open Argextend
open Tacextend
open Pcoq
View
37 interp/constrintern.ml
@@ -110,13 +110,11 @@ 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
@@ -124,10 +122,6 @@ 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
55 interp/modintern.ml
@@ -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
2 interp/notation.ml
@@ -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
1 interp/smartlocate.ml
@@ -14,7 +14,6 @@
(* *)
open Pp
open Errors
-open Util
open Libnames
open Globnames
open Misctypes
View
14 interp/topconstr.ml
@@ -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
2 intf/misctypes.mli
@@ -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
1 kernel/csymtable.ml
@@ -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
3 kernel/modops.ml
@@ -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
2 kernel/pre_env.ml
@@ -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
1 kernel/term.ml
@@ -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
2 kernel/univ.ml
@@ -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
12 lib/cList.ml
@@ -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
1 lib/dyn.ml
@@ -7,7 +7,6 @@
(************************************************************************)
open Errors
-open Util
(* Dynamics, programmed with DANGER !!! *)
View
1 lib/gmapl.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
open Util
type ('a,'b) t = ('a,'b list) Gmap.t
View
5 lib/serialize.ml
@@ -67,7 +67,6 @@ let goals : goals option call = Goal
let evars : evar list option call = Evars
let hints : (hint list * hint) option call = Hints
let status : status call = Status
-let search flags : string coq_object list call = Search flags
let get_options : (option_name * option_state) list call = GetOptions
let set_options l : unit call = SetOptions l
let inloadpath s : bool call = InLoadPath s
@@ -125,10 +124,6 @@ let do_match constr t mf = match constr with
else raise Marshal_error
| _ -> raise Marshal_error
-let pcdata = function
-| PCData s -> s
-| _ -> raise Marshal_error
-
let singleton = function
| [x] -> x
| _ -> raise Marshal_error
View
10 lib/store.ml
@@ -11,16 +11,6 @@
(* We give a short implementation of a universal type. This is mostly equivalent
to what is proposed by module Dyn.ml, except that it requires no explicit tag. *)
-module type Universal = sig
- type t
-
- type 'a etype = {
- put : 'a -> t ;
- get : t -> 'a option
- }
-
- val embed : unit -> 'a etype
-end
(* We use a dynamic "name" allocator. But if we needed to serialise stores, we
might want something static to avoid troubles with plugins order. *)
View
2 lib/system.ml
@@ -92,8 +92,6 @@ let is_in_path lpath filename =
try ignore (where_in_path ~warn:false lpath filename); true
with Not_found -> false
-let path_separator = if Sys.os_type = "Unix" then ':' else ';'
-
let is_in_system_path filename =
let path = try Sys.getenv "PATH"
with Not_found -> error "system variable PATH not found" in
View
5 lib/util.ml
@@ -24,11 +24,6 @@ let pi1 (a,_,_) = a
let pi2 (_,a,_) = a
let pi3 (_,_,a) = a
-(* Projection operator *)
-
-let down_fst f x = f (fst x)
-let down_snd f x = f (snd x)
-
(* Characters *)
let is_letter c = (c >= 'a' && c <= 'z') or (c >= 'A' && c <= 'Z')
View
1 lib/xml_parser.ml
@@ -98,7 +98,6 @@ let make source =
}
let check_eof p v = p.check_eof <- v
-let concat_pcdata p v = p.concat_pcdata <- v
let pop s =
try
View
1 library/declaremods.ml
@@ -15,7 +15,6 @@ open Entries
open Libnames
open Libobject
open Lib
-open Nametab
open Mod_subst
(** Rigid / flexible signature *)
View
1 library/dischargedhypsmap.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Util
open Libnames
type discharged_hyps = full_path list
View
1 library/global.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Util
open Names
open Term
open Environ
View
1 library/globnames.ml
@@ -7,7 +7,6 @@
(************************************************************************)
open Errors
-open Util
open Names
open Term
open Mod_subst
View
2 library/goptions.ml
@@ -199,8 +199,6 @@ type 'a option_sig = {
optread : unit -> 'a;
optwrite : 'a -> unit }
-type option_type = bool * (unit -> option_value) -> (option_value -> unit)
-
module OptionMap =
Map.Make (struct type t = option_name let compare = compare end)
View
2 library/impargs.ml
@@ -377,8 +377,6 @@ let compute_semi_auto_implicits env f manual t =
let _,autoimpls = compute_auto_implicits env f f.auto t in
[DefaultImpArgs, set_manual_implicits env f f.auto autoimpls manual]
-let compute_implicits env t = compute_semi_auto_implicits env !implicit_args [] t
-
(*s Constants. *)
let compute_constant_implicits flags manual cst =
View
13 library/lib.ml
@@ -166,13 +166,6 @@ let find_entry_p p =
in
find !lib_stk
-let find_split_p p =
- let rec find = function
- | [] -> raise Not_found
- | ent::l -> if p ent then ent,l else find l
- in
- find !lib_stk
-
let split_lib_gen test =
let rec collect after equal = function
| hd::before when test hd -> collect after (hd::equal) before
@@ -571,12 +564,10 @@ let set_lib_stk new_lib_stk =
with
| Not_found -> error "Tried to set environment to an incoherent state."
-let reset_to_gen test =
+let reset_to test =
let (_,_,before) = split_lib_gen test in
set_lib_stk before
-let reset_to sp = reset_to_gen (fun x -> fst x = sp)
-
let first_command_label = 1
let mark_end_of_command, current_command_label, reset_command_label =
@@ -599,7 +590,7 @@ let is_label_n n x =
let reset_label n =
if n >= current_command_label () then
error "Cannot backtrack to the current label or a future one";
- reset_to_gen (is_label_n n);
+ reset_to (is_label_n n);
(* forget state numbers after n only if reset succeeded *)
reset_command_label n
View
1 library/libobject.ml
@@ -7,7 +7,6 @@
(************************************************************************)
open Errors
-open Util
open Libnames
open Mod_subst
View
2 library/library.ml
@@ -496,8 +496,6 @@ let rec_intern_library_from_file idopt f =
which recursively loads its dependencies)
*)
-type library_reference = dir_path list * bool option
-
let register_library m =
Declaremods.register_library
m.library_name
View
4 parsing/egramcoq.ml
@@ -272,9 +272,9 @@ let recover_notation_grammar ntn prec =
(* Summary functions: the state of the lexer is included in that of the parser.
Because the grammar affects the set of keywords when adding or removing
grammar rules. *)
-type frozen_t = all_grammar_command list * Lexer.frozen_t
+type frozen_t = (int * all_grammar_command) list * Lexer.frozen_t
-let freeze () = (!grammar_state, Lexer.freeze ())
+let freeze () : frozen_t = (!grammar_state, Lexer.freeze ())
(* We compare the current state of the grammar and the state to unfreeze,
by computing the longest common suffixes *)
View
8 parsing/extrawit.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
-open Util
open Genarg
(* This file defines extra argument types *)
@@ -30,7 +28,7 @@ let wit_tactic = function
| 3 -> wit_tactic3
| 4 -> wit_tactic4
| 5 -> wit_tactic5
- | n -> anomaly ("Unavailable tactic level: "^string_of_int n)
+ | n -> Errors.anomaly ("Unavailable tactic level: "^string_of_int n)
let globwit_tactic = function
| 0 -> globwit_tactic0
@@ -39,7 +37,7 @@ let globwit_tactic = function
| 3 -> globwit_tactic3
| 4 -> globwit_tactic4
| 5 -> globwit_tactic5
- | n -> anomaly ("Unavailable tactic level: "^string_of_int n)
+ | n -> Errors.anomaly ("Unavailable tactic level: "^string_of_int n)
let rawwit_tactic = function
| 0 -> rawwit_tactic0
@@ -48,7 +46,7 @@ let rawwit_tactic = function
| 3 -> rawwit_tactic3
| 4 -> rawwit_tactic4
| 5 -> rawwit_tactic5
- | n -> anomaly ("Unavailable tactic level: "^string_of_int n)
+ | n -> Errors.anomaly ("Unavailable tactic level: "^string_of_int n)
let tactic_genarg_level s =
if String.length s = 7 && String.sub s 0 6 = "tactic" then
View
2 parsing/g_ltac.ml4
@@ -6,10 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pp
open Constrexpr
open Tacexpr
-open Vernacexpr
open Misctypes
open Genredexpr
open Tok
View
11 parsing/g_obligations.ml4
@@ -13,12 +13,6 @@
Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *)
-open Flags
-open Util
-open Names
-open Nameops
-open Reduction
-open Term
open Libnames
open Constrexpr
open Constrexpr_ops
@@ -38,13 +32,8 @@ struct
let withtac : Tacexpr.raw_tactic_expr option Gram.entry = gec "withtac"
end
-open Glob_term
open ObligationsGram
-open Util
-open Tok
open Pcoq
-open Prim
-open Constr
let sigref = mkRefC (Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Init.Specif.sig"))
View
2 parsing/g_vernac.ml4
@@ -18,8 +18,6 @@ open Extend
open Vernacexpr
open Locality
open Decl_kinds
-open Genarg
-open Goptions
open Declaremods
open Misctypes
View
2 parsing/g_xml.ml4
@@ -10,10 +10,8 @@ open Pp
open Errors
open Util
open Names
-open Term
open Pcoq
open Glob_term
-open Genarg
open Tacexpr
open Libnames
open Globnames
View
6 parsing/pcoq.ml4
@@ -11,11 +11,7 @@ open Compat
open Tok
open Errors
open Util
-open Names
open Extend
-open Libnames
-open Glob_term
-open Topconstr
open Genarg
open Tacexpr
open Extrawit
@@ -111,7 +107,6 @@ let weaken_entry x = Gramobj.weaken_entry x
module type Gramtypes =
sig
- open Decl_kinds
val inGramObj : 'a raw_abstract_argument_type -> 'a G.entry -> typed_entry
val outGramObj : 'a raw_abstract_argument_type -> typed_entry -> 'a G.entry
end
@@ -475,7 +470,6 @@ let level_stack =
(* At a same level, LeftA takes precedence over RightA and NoneA *)
(* In case, several associativity exists for a level, we make two levels, *)
(* first LeftA, then RightA and NoneA together *)
-open Ppextend
let admissible_assoc = function
| LeftA, Some (RightA | NonA) -> false
View
2 plugins/cc/ccalgo.ml
@@ -58,8 +58,6 @@ module ST=struct
let query sign st=Hashtbl.find st.toterm sign
- let rev_query term st=Hashtbl.find st.tosign term
-
let delete st t=
try let sign=Hashtbl.find st.tosign t in
Hashtbl.remove st.toterm sign;
View
1 plugins/cc/ccproof.ml
@@ -10,7 +10,6 @@
(* proof-trees that will be transformed into proof-terms in cctac.ml4 *)
open Errors
-open Util
open Names
open Term
open Ccalgo
View
2 plugins/cc/g_congruence.ml4
@@ -9,8 +9,6 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
open Cctac
-open Tactics
-open Tacticals
(* Tactic registration *)
View
1 plugins/decl_mode/decl_mode.ml
@@ -12,7 +12,6 @@ open Evd
open Errors
open Util
-
let daimon_flag = ref false
let set_daimon_flag () = daimon_flag:=true
View
17 plugins/decl_mode/decl_proof_instr.ml
@@ -11,7 +11,6 @@ open Util
open Pp
open Evd
-open Proof_type
open Tacmach
open Tacinterp
open Decl_expr
@@ -129,22 +128,6 @@ let daimon_tac gls =
set_daimon_flag ();
{it=[];sigma=sig_sig gls}
-
-(* marking closed blocks *)
-
-let rec is_focussing_instr = function
- Pthus i | Pthen i | Phence i -> is_focussing_instr i
- | Pescape | Pper _ | Pclaim _ | Pfocus _
- | Psuppose _ | Pcase (_,_,_) -> true
- | _ -> false
-
-let mark_rule_as_done = function
- Decl_proof true -> Decl_proof false
- | Decl_proof false ->
- anomaly "already marked as done"
- | _ -> anomaly "mark_rule_as_done"
-
-
(* post-instruction focus management *)
(* spiwack: This used to fail if there was no focusing command
View
3 plugins/decl_mode/g_decl_mode.ml4
@@ -14,13 +14,10 @@ open Pp
open Tok
open Decl_expr
open Names
-open Term
-open Genarg
open Pcoq
open Pcoq.Constr
open Pcoq.Tactic
-open Pcoq.Vernac_
let pr_goal gs =
let (g,sigma) = Goal.V82.nf_evar (Tacmach.project gs) (Evd.sig_it gs) in
View
1 plugins/decl_mode/ppdecl_proof.ml
@@ -7,7 +7,6 @@
(************************************************************************)
open Errors
-open Util
open Pp
open Decl_expr
open Names
View
10 plugins/extraction/extract_env.ml
@@ -70,16 +70,12 @@ module type VISIT = sig
(* Reset the dependencies by emptying the visit lists *)
val reset : unit -> unit
- (* Add the module_path and all its prefixes to the mp visit list *)
- val add_mp : module_path -> unit
-
- (* Same, but we'll keep all fields of these modules *)
+ (* Add the module_path and all its prefixes to the mp visit list.
+ We'll keep all fields of these modules. *)
val add_mp_all : module_path -> unit
- (* Add kernel_name / constant / reference / ... in the visit lists.
+ (* Add reference / ... in the visit lists.
These functions silently add the mp of their arg in the mp list *)
- val add_ind : mutual_inductive -> unit
- val add_con : constant -> unit
val add_ref : global_reference -> unit
val add_decl_deps : ml_decl -> unit
val add_spec_deps : ml_spec -> unit
View
2 plugins/extraction/g_extraction.ml4
@@ -10,8 +10,6 @@
(* ML names *)
-open Vernacexpr
-open Pcoq
open Genarg
open Pp
open Names
View
5 plugins/extraction/haskell.ml
@@ -13,7 +13,6 @@ open Errors
open Util
open Names
open Nameops
-open Libnames
open Globnames
open Table
open Miniml
@@ -82,10 +81,6 @@ let pp_global k r =
(*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
are needed or not. *)
-let kn_sig =
- let specif = MPfile (dirpath_of_string "Coq.Init.Specif") in
- make_mind specif empty_dirpath (mk_label "sig")
-
let rec pp_type par vl t =
let rec pp_rec par = function
| Tmeta _ | Tvar' _ -> assert false
View
15 plugins/extraction/mlutil.ml
@@ -224,21 +224,6 @@ let type_maxvar t =
| _ -> n
in parse 0 t
-(*s What are the type variables occurring in [t]. *)
-
-let intset_union_map_list f l =
- List.fold_left (fun s t -> Intset.union s (f t)) Intset.empty l
-
-let intset_union_map_array f a =
- Array.fold_left (fun s t -> Intset.union s (f t)) Intset.empty a
-
-let rec type_listvar = function
- | Tmeta {contents = Some t} -> type_listvar t
- | Tvar i | Tvar' i -> Intset.singleton i
- | Tarr (a,b) -> Intset.union (type_listvar a) (type_listvar b)
- | Tglob (_,l) -> intset_union_map_list type_listvar l
- | _ -> Intset.empty
-
(*s From [a -> b -> c] to [[a;b],c]. *)
let rec type_decomp = function
View
2 plugins/extraction/modutil.ml
@@ -289,8 +289,6 @@ and optim_me to_appear s = function
For non-library extraction, we recompute a minimal set of dependencies
for first-level objects *)
-exception NoDepCheck
-
let base_r = function
| ConstRef c as r -> r
| IndRef (kn,_) -> IndRef (kn,0)
View
3 plugins/firstorder/g_ground.ml4
@@ -12,11 +12,8 @@ open Formula
open Sequent
open Ground
open Goptions
-open Tactics
open Tacticals
open Tacinterp
-open Term
-open Names
open Libnames
(* declaring search depth as a global option *)
View
4 plugins/firstorder/sequent.ml
@@ -48,8 +48,6 @@ let priority = (* pure heuristics, <=0 for non reversible *)
| LLexists (_,_) -> 50
| LLarrow (_,_,_) -> -10
-let left_reversible lpat=(priority lpat)>0
-
module OrderedFormula=
struct
type t=Formula.t
@@ -163,8 +161,6 @@ let find_left t seq=List.hd (CM.find t seq.context)
left_reversible lpat
with Heap.EmptyHeap -> false
*)
-let no_formula seq=
- seq.redexes=HP.empty
let rec take_formula seq=
let hd=HP.maximum seq.redexes
View
2 plugins/fourier/fourierR.ml
@@ -14,7 +14,6 @@ des in
open Term
open Tactics
-open Clenv
open Names
open Libnames
open Globnames
@@ -76,7 +75,6 @@ let flin_emult a f =
;;
(*****************************************************************************)
-open Vernacexpr
type ineq = Rlt | Rle | Rgt | Rge
View
38 plugins/funind/functional_principles_proofs.ml
@@ -134,19 +134,6 @@ let refine c =
let thin l =
Tacmach.thin_no_check l
-
-let cut_replacing id t tac :tactic=
- tclTHENS (cut t)
- [ tclTHEN (thin_no_check [id]) (introduction_no_check id);
- tac
- ]
-
-let intro_erasing id = tclTHEN (thin [id]) (introduction id)
-
-
-
-let rec_hyp_id = id_of_string "rec_hyp"
-
let is_trivial_eq t =
let res = try
begin
@@ -367,7 +354,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type =
new_ctxt,new_end_of_type,simpl_eq_tac
-let is_property ptes_info t_x full_type_of_hyp =
+let is_property (ptes_info:ptes_info) t_x full_type_of_hyp =
if isApp t_x
then
let pte,args = destApp t_x in
@@ -563,7 +550,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
thin [hyp_id],[]
-let clean_goal_with_heq ptes_infos continue_tac dyn_infos =
+let clean_goal_with_heq ptes_infos continue_tac (dyn_infos:body_info) =
fun g ->
let env = pf_env g
and sigma = project g
@@ -894,13 +881,6 @@ let build_proof
(* Proof of principles from structural functions *)
-let is_pte_type t =
- isSort ((strip_prod t))
-
-let is_pte (_,_,t) = is_pte_type t
-
-
-
type static_fix_info =
{
@@ -932,9 +912,6 @@ let prove_rec_hyp fix_info =
is_valid = fun _ -> true
}
-
-exception Not_Rec
-
let generalize_non_dep hyp g =
(* observe (str "rec id := " ++ Ppconstr.pr_id hyp); *)
let hyps = [hyp] in
@@ -1427,17 +1404,6 @@ let backtrack_eqs_until_hrec hrec eqs : tactic =
backtrack gls
-
-let build_clause eqs =
- {
- Locus.onhyps =
- Some (List.map
- (fun id -> (Locus.AllOccurrences, id), Locus.InHyp)
- eqs
- );
- Locus.concl_occs = Locus.NoOccurrences
- }
-
let rec rewrite_eqs_in_eqs eqs =
match eqs with
| [] -> tclIDTAC
View
16 plugins/funind/functional_principles_types.ml
@@ -289,22 +289,6 @@ let change_property_sort toSort princ princName =
let pp_dur time time' =
str (string_of_float (System.time_difference time time'))
-(* let qed () = save_named true *)
-let defined () =
- try
- Lemmas.save_named false
- with
- | UserError("extract_proof",msg) ->
- Errors.errorlabstrm
- "defined"
- ((try
- str "On goal : " ++ fnl () ++ pr_open_subgoals () ++ fnl ()
- with _ -> mt ()
- ) ++msg)
- | e -> raise e
-
-
-
let build_functional_principle interactive_proof old_princ_type sorts funs i proof_tac hook =
(* First we get the type of the old graph principle *)
let mutr_nparams = (compute_elim_sig old_princ_type).nparams in
View
2 plugins/funind/g_indfun.ml4
@@ -14,9 +14,7 @@ open Constrexpr
open Indfun_common
open Indfun
open Genarg
-open Pcoq
open Tacticals
-open Constr
open Misctypes
open Miscops
View
38 plugins/funind/glob_term_to_relation.ml
@@ -288,10 +288,6 @@ let make_discr_match brl =
make_discr_match_el el,
make_discr_match_brl i brl)
-let pr_name = function
- | Name id -> Ppconstr.pr_id id
- | Anonymous -> str "_"
-
(**********************************************************************)
(* functions used to build case expression from lettuple and if ones *)
(**********************************************************************)
@@ -326,40 +322,6 @@ let build_constructors_of_type ind' argl =
)
ind.Declarations.mind_consnames
-(* [find_type_of] very naive attempts to discover the type of an if or a letin *)
-let rec find_type_of nb b =
- let f,_ = glob_decompose_app b in
- match f with
- | GRef(_,ref) ->
- begin
- let ind_type =
- match ref with
- | VarRef _ | ConstRef _ ->
- let constr_of_ref = constr_of_global ref in
- let type_of_ref = Typing.type_of (Global.env ()) Evd.empty constr_of_ref in
- let (_,ret_type) = Reduction.dest_prod (Global.env ()) type_of_ref in
- let ret_type,_ = decompose_app ret_type in
- if not (isInd ret_type) then
- begin
-(* Pp.msgnl (str "not an inductive" ++ pr_lconstr ret_type); *)
- raise (Invalid_argument "not an inductive")
- end;
- destInd ret_type
- | IndRef ind -> ind
- | ConstructRef c -> fst c
- in
- let _,ind_type_info = Inductive.lookup_mind_specif (Global.env()) ind_type in
- if not (Array.length ind_type_info.Declarations.mind_consnames = nb )
- then raise (Invalid_argument "find_type_of : not a valid inductive");
- ind_type
- end
- | GCast(_,b,_) -> find_type_of nb b
- | GApp _ -> assert false (* we have decomposed any application via glob_decompose_app *)
- | _ -> raise (Invalid_argument "not a ref")
-
-
-
-
(******************)
(* Main functions *)
(******************)
View
60 plugins/funind/indfun.ml
@@ -21,7 +21,7 @@ let is_rec_info scheme_info =
Util.Intset.exists (fun i -> i >= min && i< max) free_rels_in_br
)
in
- Util.List.fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches)
+ List.fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches)
let choose_dest_or_ind scheme_info =
if is_rec_info scheme_info
@@ -496,64 +496,6 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
let map_option f = function
| None -> None
| Some v -> Some (f v)
-
-let decompose_lambda_n_assum_constr_expr =
- let rec decompose_lambda_n_assum_constr_expr acc n e =
- if n = 0 then (List.rev acc,e)
- else
- match e with
- | Constrexpr.CLambdaN(_, [],e') -> decompose_lambda_n_assum_constr_expr acc n e'
- | Constrexpr.CLambdaN(lambda_loc,(nal,bk,nal_type)::bl,e') ->
- let nal_length = List.length nal in
- if nal_length <= n
- then
- decompose_lambda_n_assum_constr_expr
- (Constrexpr.LocalRawAssum(nal,bk,nal_type)::acc)
- (n - nal_length)
- (Constrexpr.CLambdaN(lambda_loc,bl,e'))
- else
- let nal_keep,nal_expr = List.chop n nal in
- (List.rev (Constrexpr.LocalRawAssum(nal_keep,bk,nal_type)::acc),
- Constrexpr.CLambdaN(lambda_loc,(nal_expr,bk,nal_type)::bl,e')
- )
- | Constrexpr.CLetIn(_, na,nav,e') ->
- decompose_lambda_n_assum_constr_expr
- (Constrexpr.LocalRawDef(na,nav)::acc) (pred n) e'
- | _ -> error "Not enough product or assumption"
- in
- decompose_lambda_n_assum_constr_expr []
-
-let decompose_prod_n_assum_constr_expr =
- let rec decompose_prod_n_assum_constr_expr acc n e =
- (* Pp.msgnl (str "n := " ++ int n ++ fnl ()++ *)
- (* str "e := " ++ Ppconstr.pr_lconstr_expr e); *)
- if n = 0 then
- (* let _ = Pp.msgnl (str "return_type := " ++ Ppconstr.pr_lconstr_expr e) in *)
- (List.rev acc,e)
- else
- match e with
- | Constrexpr.CProdN(_, [],e') -> decompose_prod_n_assum_constr_expr acc n e'
- | Constrexpr.CProdN(lambda_loc,(nal,bk,nal_type)::bl,e') ->
- let nal_length = List.length nal in
- if nal_length <= n
- then
- (* let _ = Pp.msgnl (str "first case") in *)
- decompose_prod_n_assum_constr_expr
- (Constrexpr.LocalRawAssum(nal,bk,nal_type)::acc)
- (n - nal_length)
- (if bl = [] then e' else (Constrexpr.CLambdaN(lambda_loc,bl,e')))
- else
- (* let _ = Pp.msgnl (str "second case") in *)
- let nal_keep,nal_expr = List.chop n nal in
- (List.rev (Constrexpr.LocalRawAssum(nal_keep,bk,nal_type)::acc),
- Constrexpr.CLambdaN(lambda_loc,(nal_expr,bk,nal_type)::bl,e')
- )
- | Constrexpr.CLetIn(_, na,nav,e') ->
- decompose_prod_n_assum_constr_expr
- (Constrexpr.LocalRawDef(na,nav)::acc) (pred n) e'
- | _ -> error "Not enough product or assumption"
- in
- decompose_prod_n_assum_constr_expr []
open Constrexpr
open Topconstr
View
13 plugins/funind/indfun_common.ml
@@ -131,12 +131,6 @@ let coq_constant s =
Coqlib.gen_constant_in_modules "RecursiveDefinition"
Coqlib.init_modules s;;
-let constant sl s =
- constr_of_global
- (Nametab.locate (make_qualid(Names.make_dirpath
- (List.map id_of_string (List.rev sl)))
- (id_of_string s)));;
-
let find_reference sl s =
(Nametab.locate (make_qualid(Names.make_dirpath
(List.map id_of_string (List.rev sl)))
@@ -277,7 +271,6 @@ let cache_Function (_,finfos) =
let load_Function _ = cache_Function
-let open_Function _ = cache_Function
let subst_Function (subst,finfos) =
let do_subst_con c = fst (Mod_subst.subst_con subst c)
and do_subst_ind (kn,i) = (Mod_subst.subst_ind subst kn,i)
@@ -508,12 +501,6 @@ let jmeq () =
init_constant ["Logic";"JMeq"] "JMeq")
with e -> raise (ToShow e)
-let jmeq_rec () =
- try
- Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
- init_constant ["Logic";"JMeq"] "JMeq_rec"
- with e -> raise (ToShow e)
-
let jmeq_refl () =
try
Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
View
11 plugins/funind/merge.ml
@@ -853,17 +853,6 @@ let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
lident , bindlist , Some cstr_expr , lcstor_expr
-
-let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) =
- match rdecl with
- | (nme,None,t) ->
- let traw = Detyping.detype false [] [] t in
- GProd (Loc.ghost,nme,Explicit,traw,t2)
- | (_,Some _,_) -> assert false
-
-
-
-
let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) =
match rdecl with
| (nme,None,t) ->
View
16 plugins/funind/recdef.ml
@@ -18,7 +18,6 @@ open Globnames
open Nameops
open Errors
open Util
-open Closure
open Tacticals
open Tacmach
open Tactics
@@ -50,10 +49,6 @@ let coq_base_constant s =
Coqlib.gen_constant_in_modules "RecursiveDefinition"
(Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s;;
-let coq_constant s =
- Coqlib.gen_constant_in_modules "RecursiveDefinition"
- (Coqlib.init_modules @ Coqlib.arith_modules) s;;
-
let find_reference sl s =
(locate (make_qualid(Names.make_dirpath
(List.map id_of_string (List.rev sl)))
@@ -126,7 +121,6 @@ let compute_renamed_type gls c =
rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) []
(pf_type_of gls c)
let h'_id = id_of_string "h'"
-let heq_id = id_of_string "Heq"
let teq_id = id_of_string "teq"
let ano_id = id_of_string "anonymous"
let x_id = id_of_string "x"
@@ -154,18 +148,12 @@ let le_n = function () -> (coq_base_constant "le_n")
let coq_sig_ref = function () -> (find_reference ["Coq";"Init";"Specif"] "sig")
let coq_O = function () -> (coq_base_constant "O")
let coq_S = function () -> (coq_base_constant "S")
-let gt_antirefl = function () -> (coq_constant "gt_irrefl")
let lt_n_O = function () -> (coq_base_constant "lt_n_O")
-let lt_n_Sn = function () -> (coq_base_constant "lt_n_Sn")
-let f_equal = function () -> (coq_constant "f_equal")
-let well_founded_induction = function () -> (coq_constant "well_founded_induction")
let max_ref = function () -> (find_reference ["Recdef"] "max")
let max_constr = function () -> (constr_of_global (delayed_force max_ref))
let coq_conj = function () -> find_reference ["Coq";"Init";"Logic"] "conj"
let f_S t = mkApp(delayed_force coq_S, [|t|]);;
-let make_refl_eq constructor type_of_t t =
- mkApp(constructor,[|type_of_t;t|])
let rec n_x_id ids n =
if n = 0 then []
@@ -960,10 +948,6 @@ let equation_others _ expr_info continuation_tac infos =
(intros_values_eq expr_info [])
else continuation_tac infos
-let equation_letin (na,b,t,e) expr_info continuation_tac info =
- let new_e = subst1 info.info e in
- continuation_tac {info with info = new_e;}
-
let equation_app f_and_args expr_info continuation_tac infos =
if expr_info.is_final && expr_info.is_main_branch
then intros_values_eq expr_info []
View
4 plugins/micromega/certificate.ml
@@ -405,9 +405,7 @@ let pplus x y = Mc.PEadd(x,y)
let pmult x y = Mc.PEmul(x,y)
let pconst x = Mc.PEc x
let popp x = Mc.PEopp x
-
-let debug = false
-
+
(* keep track of enumerated vectors *)
let rec mem p x l =
match l with [] -> false | e::l -> if p x e then true else mem p x l
View
3 plugins/micromega/g_micromega.ml4
@@ -16,9 +16,6 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
-open Quote
-open Mutils
-open Glob_term
open Errors
open Misctypes
View
21 plugins/nsatz/nsatz.ml4
@@ -8,34 +8,13 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
-open Pp
open Errors
open Util
-open Names
open Term
-open Closure
-open Environ
-open Libnames
open Tactics
-open Glob_term
-open Tacticals
-open Tacexpr
-open Pcoq
-open Tactic
-open Constr
-open Proof_type
open Coqlib
-open Tacmach
-open Mod_subst
-open Tacinterp
-open Libobject
-open Printer
-open Declare
-open Decl_kinds
-open Entries
open Num
-open Unix
open Utile
(***********************************************************************
View
3 plugins/nsatz/polynom.ml
@@ -7,9 +7,8 @@
(************************************************************************)
(* Recursive polynomials: R[x1]...[xn]. *)
-open Utile
-open Errors
open Util
+open Utile
(* 1. Coefficients: R *)
View
12 plugins/omega/coq_omega.ml
@@ -15,21 +15,12 @@
open Errors
open Util
-open Pp
-open Reduction
-open Proof_type
open Names
open Nameops
open Term
-open Declarations
-open Environ
-open Sign
-open Inductive
open Tacticals
open Tacmach
-open Evar_refiner
open Tactics
-open Clenv
open Logic
open Libnames
open Globnames
@@ -193,8 +184,6 @@ let coq_Zopp = lazy (zbase_constant "Z.opp")
let coq_Zminus = lazy (zbase_constant "Z.sub")
let coq_Zsucc = lazy (zbase_constant "Z.succ")
let coq_Zpred = lazy (zbase_constant "Z.pred")
-let coq_Zgt = lazy (zbase_constant "Z.gt")
-let coq_Zle = lazy (zbase_constant "Z.le")
let coq_Z_of_nat = lazy (zbase_constant "Z.of_nat")
let coq_inj_plus = lazy (z_constant "Nat2Z.inj_add")
let coq_inj_mult = lazy (z_constant "Nat2Z.inj_mul")
@@ -326,7 +315,6 @@ let coq_iff = lazy (constant "iff")
(* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *)
(* For unfold *)
-open Closure
let evaluable_ref_of_constr s c = match kind_of_term (Lazy.force c) with
| Const kn when Tacred.is_evaluable (Global.env()) (EvalConstRef kn) ->
EvalConstRef kn
View
2 plugins/omega/omega.ml
@@ -17,8 +17,6 @@
(* the number of source of numbering. *)
(**************************************************************************)
-open Names
-
module type INT = sig
type bigint
val less_than : bigint -> bigint -> bool
View
1 plugins/quote/g_quote.ml4
@@ -8,7 +8,6 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
-open Pp
open Tacexpr
open Quote
View
3 plugins/quote/quote.ml
@@ -101,7 +101,6 @@
(*i*)
-open Pp
open Errors
open Util
open Names
@@ -110,8 +109,6 @@ open Pattern
open Patternops
open Matching
open Tacmach
-open Tactics
-open Tacexpr
(*i*)
(*s First, we need to access some Coq constants
View
1 plugins/romega/const_omega.ml
@@ -71,7 +71,6 @@ let z_constant = Coqlib.gen_constant_in_modules "Omega" z_module
let bin_constant = Coqlib.gen_constant_in_modules "Omega" bin_module
(* Logic *)
-let coq_eq = lazy(init_constant "eq")