diff options
73 files changed, 3 insertions, 164 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index dea70360a..650897ef7 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -22,7 +22,6 @@ open Evd open Goptions open Genarg open Clenv -open Universes let _ = Detyping.print_evar_arguments := true let _ = Detyping.print_universes := true diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 7b9ad3136..ff090ca84 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -10,12 +10,10 @@ open Loc open Names open Constrexpr open Libnames -open Globnames open Nametab open Genredexpr open Genarg open Pattern -open Decl_kinds open Misctypes open Locus diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index eab36d8b2..8fb6601a9 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -1,4 +1,3 @@ -open Names open Cbytecodes open Cemitcodes open Term diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 3c9692a5c..9ecae2b36 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -10,7 +10,6 @@ machine, Oct 2004 *) (* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *) -open Names open Term open Cbytecodes open Copcodes diff --git a/kernel/closure.ml b/kernel/closure.ml index f06b13d8d..6824c399e 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -771,24 +771,6 @@ let drop_parameters depth n argstk = (* we know that n < stack_args_size(argstk) (if well-typed term) *) anomaly (Pp.str "ill-typed term: found a match on a partially applied constructor") - -let rec get_parameters depth n argstk = - match argstk with - Zapp args::s -> - let q = Array.length args in - if n > q then Array.append args (get_parameters depth (n-q) s) - else if Int.equal n q then [||] - else Array.sub args 0 n - | Zshift(k)::s -> - get_parameters (depth-k) n s - | [] -> (* we know that n < stack_args_size(argstk) (if well-typed term) *) - if Int.equal n 0 then [||] - else raise Not_found (* Trying to eta-expand a partial application..., should do - eta expansion first? *) - | _ -> assert false - (* strip_update_shift_app only produces Zapp and Zshift items *) - - (** [eta_expand_ind_stack env ind c s t] computes stacks correspoding to the conversion of the eta expansion of t, considered as an inhabitant of ind, and the Constructor c of this inductive type applied to arguments diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 47a82cc6c..ce65af975 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -9,7 +9,6 @@ open Declarations open Mod_subst open Univ -open Context (** Operations concerning types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli index 4c2c92ccf..90d9c55f1 100644 --- a/kernel/fast_typeops.mli +++ b/kernel/fast_typeops.mli @@ -6,13 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names -open Univ open Term -open Context open Environ -open Entries -open Declarations (** {6 Typing functions (not yet tagged as safe) } diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 99d9f52c9..ea575e1e0 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -654,7 +654,6 @@ let used_section_variables env inds = keep_hyps env ids let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) -let rel_appvect n m = rel_vect n (List.length m) exception UndefinableExpansion diff --git a/kernel/inductive.ml b/kernel/inductive.ml index bb57ad256..6b4dd536a 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -447,13 +447,6 @@ type subterm_spec = let eq_wf_paths = Rtree.equal Declareops.eq_recarg -let pp_recarg = function - | Norec -> Pp.str "Norec" - | Mrec i -> Pp.str ("Mrec "^MutInd.to_string (fst i)) - | Imbr i -> Pp.str ("Imbr "^MutInd.to_string (fst i)) - -let pp_wf_paths = Rtree.pp_tree pp_recarg - let inter_recarg r1 r2 = match r1, r2 with | Norec, Norec -> Some r1 | Mrec i1, Mrec i2 diff --git a/kernel/names.ml b/kernel/names.ml index b349ccb00..4ccf5b60a 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -571,7 +571,6 @@ let constr_modpath (ind,_) = ind_modpath ind let ith_mutual_inductive (mind, _) i = (mind, i) let ith_constructor_of_inductive ind i = (ind, i) -let ith_constructor_of_pinductive (ind,u) i = ((ind,i),u) let inductive_of_constructor (ind, i) = ind let index_of_constructor (ind, i) = i diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 1a4a4b54d..ada7ae737 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -12,7 +12,6 @@ open Context open Declarations open Util open Nativevalues -open Primitives open Nativeinstr open Nativelambda open Pre_env diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 6a97edc40..ccf2888b5 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -8,7 +8,6 @@ open Names open Term open Pre_env -open Nativevalues open Nativeinstr (** This file defines the lambda code generation phase of the native compiler *) diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml index 914f577e2..0b8662ff0 100644 --- a/kernel/nativelibrary.ml +++ b/kernel/nativelibrary.ml @@ -12,7 +12,6 @@ open Environ open Mod_subst open Modops open Nativecode -open Nativelib (** This file implements separate compilation for libraries in the native compiler *) diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 87cebd62f..0609c8517 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -9,7 +9,6 @@ open Names open Term open Mod_subst -open Int (** This module implements the handling of opaque proof terms. Opauqe proof terms are special since: diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 4153b323b..b09367dd9 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -28,14 +28,6 @@ open Esubst let left2right = ref false -let conv_key k = - match k with - VarKey id -> - VarKey id - | ConstKey (cst,_) -> - ConstKey cst - | RelKey n -> RelKey n - let rec is_empty_stack = function [] -> true | Zupdate _::s -> is_empty_stack s diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index a3441aa3e..b54511e40 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -15,7 +15,6 @@ open Errors open Util open Names -open Univ open Term open Context open Declarations @@ -101,10 +100,6 @@ let hcons_j j = let feedback_completion_typecheck = Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete) - -let subst_instance_j s j = - { uj_val = Vars.subst_univs_level_constr s j.uj_val; - uj_type = Vars.subst_univs_level_constr s j.uj_type } let infer_declaration env kn dcl = match dcl with diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 696fc3d2d..1b54b1ea1 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -8,7 +8,6 @@ open Names open Term -open Univ open Environ open Declarations open Entries diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 80b15f8ba..29315b0a9 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -42,8 +42,6 @@ let conv_vect fconv vect1 vect2 cu = let infos = ref (create_clos_infos betaiotazeta Environ.empty_env) -let eq_table_key = Names.eq_table_key eq_constant - let rec conv_val env pb k v1 v2 cu = if v1 == v2 then cu else conv_whd env pb k (whd_val v1) (whd_val v2) cu diff --git a/lib/monad.ml b/lib/monad.ml index 4a52684da..a1714a41b 100644 --- a/lib/monad.ml +++ b/lib/monad.ml @@ -111,7 +111,7 @@ module Make (M:Def) : S with type +'a t = 'a M.t = struct | [a] -> M.map (fun a' -> [a']) (f a) | a::b::l -> - map f l >>= fun l' -> + map_right f l >>= fun l' -> f b >>= fun b' -> M.map (fun a' -> a'::b'::l') (f a) @@ -387,8 +387,6 @@ let pp_with ?pp_tag ft strm = let ppnl_with ft strm = pp_dirs ft (Glue.atom (Ppdir_ppcmds (strm ++ fnl ()))) -let pp_flush_with ft = Format.pp_print_flush ft - (* pretty printing functions WITH FLUSH *) let msg_with ft strm = pp_dirs ft (Glue.atom(Ppdir_ppcmds strm) ++ Glue.atom(Ppdir_print_flush)) diff --git a/library/globnames.ml b/library/globnames.ml index 5eb091af4..3befaa9a9 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util open Errors open Names open Term diff --git a/library/library.ml b/library/library.ml index b078e2c47..16dedf565 100644 --- a/library/library.ml +++ b/library/library.ml @@ -402,9 +402,6 @@ let intern_from_file f = module DPMap = Map.Make(DirPath) -let deps_to_string deps = - Array.fold_left (fun s (n, _) -> s^"\n - "^(DirPath.to_string n)) "" deps - let rec intern_library (needed, contents) (dir, f) from = Pp.feedback(Feedback.FileDependency (from, f)); (* Look if in the current logical environment *) diff --git a/library/universes.mli b/library/universes.mli index f2f68d329..252648d7d 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -7,12 +7,9 @@ (************************************************************************) open Util -open Pp open Names open Term -open Context open Environ -open Locus open Univ (** Universes *) diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli index 0e0eb6d2a..2ff2bd387 100644 --- a/plugins/cc/ccproof.mli +++ b/plugins/cc/ccproof.mli @@ -7,7 +7,6 @@ (************************************************************************) open Ccalgo -open Names open Term type rule= diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli index 29ea1e777..6c7b09383 100644 --- a/plugins/firstorder/formula.mli +++ b/plugins/firstorder/formula.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Term open Context open Globnames diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 8006a3e13..7a56cd665 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -16,7 +16,6 @@ open Term open Tactics open Names open Globnames -open Tacticals open Tacmach open Fourier open Contradiction diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index c8214ada8..eb5221fd6 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -7,7 +7,6 @@ open Context open Namegen open Names open Declarations -open Declareops open Pp open Tacmach open Proof_type @@ -16,7 +15,6 @@ open Tactics open Indfun_common open Libnames open Globnames -open Misctypes (* let msgnl = Pp.msgnl *) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 545f8931f..80167686a 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -6,7 +6,6 @@ open Vars open Context open Namegen open Names -open Declareops open Pp open Entries open Tactics diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 6dbd61cfd..2730fd421 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -8,7 +8,6 @@ open Libnames open Globnames open Glob_term open Declarations -open Declareops open Misctypes open Decl_kinds diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 53f8b0db8..b6c5d426f 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -12,7 +12,6 @@ open Names open Term open Context open Environ -open Mod_subst (** {5 Existential variables and unification states} diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index 7f7f4d764..95a6ba79d 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -11,7 +11,6 @@ open Util open Errors open Names open Locus -open Context open Term open Nameops open Termops diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli index 82330b846..47d9654e5 100644 --- a/pretyping/find_subterm.mli +++ b/pretyping/find_subterm.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Locus open Context open Term diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 654f914b6..adf714db3 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -18,7 +18,6 @@ open Declarations open Declareops open Environ open Reductionops -open Inductive (* The following three functions are similar to the ones defined in Inductive, but they expect an env *) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index b4e0459c1..1106fefa3 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -23,7 +23,6 @@ open Reductionops open Cbv open Patternops open Locus -open Pretype_errors (* Errors *) diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 5862a8525..9f04faa83 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -15,7 +15,6 @@ open Term open Vars open Context open Environ -open Locus (* Sorts and sort family *) diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 9f3efd72b..2552c67e6 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -11,7 +11,6 @@ open Names open Term open Context open Environ -open Locus (** printers *) val print_sort : sorts -> std_ppcmds diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 817d68782..b64ccf60d 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -14,7 +14,6 @@ open Term open Vars open Context open Evd -open Environ open Util open Typeclasses_errors open Libobject @@ -427,7 +426,6 @@ let add_class cl = cl.cl_projs -open Declarations (* * interface functions diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index 4f88dd860..585f066db 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -10,7 +10,6 @@ open Names open Term open Context -open Evd open Environ open Constrexpr open Globnames diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index dd8087713..7982fc852 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -10,7 +10,6 @@ open Loc open Names open Term open Context -open Evd open Environ open Constrexpr open Globnames diff --git a/pretyping/typing.mli b/pretyping/typing.mli index c933106d7..1f822f1a5 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Term open Environ open Evd diff --git a/printing/ppconstrsig.mli b/printing/ppconstrsig.mli index 15413d515..b7eb9b1ff 100644 --- a/printing/ppconstrsig.mli +++ b/printing/ppconstrsig.mli @@ -12,8 +12,6 @@ open Libnames open Constrexpr open Names open Misctypes -open Locus -open Genredexpr module type Pp = sig diff --git a/printing/pptactic.mli b/printing/pptactic.mli index 284237f01..a0bbc2e79 100644 --- a/printing/pptactic.mli +++ b/printing/pptactic.mli @@ -15,9 +15,6 @@ open Names open Constrexpr open Tacexpr open Ppextend -open Environ -open Pattern -open Misctypes type 'a raw_extra_genarg_printer = (constr_expr -> std_ppcmds) -> diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli index 98b5757da..166a6675c 100644 --- a/printing/pptacticsig.mli +++ b/printing/pptacticsig.mli @@ -8,7 +8,6 @@ open Pp open Genarg -open Names open Constrexpr open Tacexpr open Ppextend diff --git a/printing/printer.ml b/printing/printer.ml index 8a2d6e7bd..fb98f6073 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -11,7 +11,6 @@ open Errors open Util open Names open Term -open Vars open Environ open Globnames open Nametab diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 9b671bcf0..eb1081706 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -10,7 +10,6 @@ open Names open Term open Environ open Evd -open Mod_subst open Unification open Misctypes diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index da40427c4..ea2043613 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -8,7 +8,6 @@ open Term open Clenv -open Proof_type open Tacexpr open Unification diff --git a/proofs/goal.ml b/proofs/goal.ml index e3570242e..107ce7f8e 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -9,8 +9,6 @@ open Util open Pp open Term -open Vars -open Context (* This module implements the abstract interface to goals *) (* A general invariant of the module, is that a goal whose associated diff --git a/proofs/logic.ml b/proofs/logic.ml index 53f8093e5..b8206ca1b 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -13,7 +13,6 @@ open Names open Nameops open Term open Vars -open Context open Termops open Environ open Reductionops @@ -83,12 +82,6 @@ let apply_to_hyp sign id f = if !check then error_no_such_hypothesis id else sign -let apply_to_hyp_and_dependent_on sign id f g = - try apply_to_hyp_and_dependent_on sign id f g - with Hyp_not_found -> - if !check then error_no_such_hypothesis id - else sign - let check_typability env sigma c = if !check then let _ = type_of env sigma c in () @@ -277,11 +270,6 @@ let move_hyp toleft (left,(idfrom,_,_ as declfrom),right) hto = List.fold_left (fun sign d -> push_named_context_val d sign) right left -let rename_hyp id1 id2 sign = - apply_to_hyp_and_dependent_on sign id1 - (fun (_,b,t) _ -> (id2,b,t)) - (fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d) - (**********************************************************************) diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 26bb78dfe..47b2b255e 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -10,7 +10,6 @@ open Evd open Names open Term -open Context open Tacexpr open Glob_term open Nametab diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index e709be5bc..f5e2bad2a 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -9,7 +9,6 @@ open Evd open Names open Term -open Context open Tacexpr open Glob_term open Nametab diff --git a/stm/lemmas.mli b/stm/lemmas.mli index d0669d7a3..a0ddd265c 100644 --- a/stm/lemmas.mli +++ b/stm/lemmas.mli @@ -10,7 +10,6 @@ open Names open Term open Decl_kinds open Constrexpr -open Tacexpr open Vernacexpr open Pfedit diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index d71c169d6..a0979f8b1 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -15,7 +15,6 @@ open Bigint open Decl_kinds open Extend open Libnames -open Flags let unlock loc = let start, stop = Loc.unloc loc in diff --git a/tactics/auto.mli b/tactics/auto.mli index ea3f0ac0d..0cc8a0b1b 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -8,7 +8,6 @@ open Names open Term -open Proof_type open Clenv open Pattern open Evd diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 1c15fa40b..e97a42e6e 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -17,7 +17,6 @@ open Proof_type open Tacticals open Tacmach open Tactics -open Patternops open Clenv open Typeclasses open Globnames @@ -42,7 +41,7 @@ let get_typeclasses_dependency_order () = !typeclasses_dependency_order open Goptions -let set_typeclasses_modulo_eta = +let _ = declare_bool_option { optsync = true; optdepr = false; @@ -51,7 +50,7 @@ let set_typeclasses_modulo_eta = optread = get_typeclasses_modulo_eta; optwrite = set_typeclasses_modulo_eta; } -let set_typeclasses_dependency_order = +let _ = declare_bool_option { optsync = true; optdepr = false; diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 9ee14b801..9b69481da 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -9,8 +9,6 @@ open Errors open Term open Hipattern -open Tacmach -open Tacticals open Tactics open Coqlib open Reductionops diff --git a/tactics/eauto.mli b/tactics/eauto.mli index 19e2f198b..7073e8a2b 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -8,7 +8,6 @@ open Term open Proof_type -open Auto open Evd open Hints diff --git a/tactics/elim.ml b/tactics/elim.ml index b7d5b1028..3cb4fa9c4 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -15,7 +15,6 @@ open Hipattern open Tacmach.New open Tacticals.New open Tactics -open Misctypes open Proofview.Notations let introElimAssumsThen tac ba = diff --git a/tactics/equality.ml b/tactics/equality.ml index c130fa151..ae92f4c06 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -487,9 +487,6 @@ let apply_special_clear_request clear_flag f = e when catchable_exception e -> tclIDTAC end -type delayed_open_constr_with_bindings = - env -> evar_map -> evar_map * constr with_bindings - let general_multi_rewrite with_evars l cl tac = let do1 l2r f = Proofview.Goal.enter begin fun gl -> @@ -1474,8 +1471,6 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b = (* then it uses the predicate "\x.phi(proj1_sig x,proj2_sig x)", and so *) (* on for further iterated sigma-tuples *) -exception NothingToRewrite - let cutSubstInConcl l2r eqn = Proofview.Goal.nf_enter begin fun gl -> let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in @@ -1513,9 +1508,6 @@ let try_rewrite tac = | e when catchable_exception e -> tclZEROMSG (strbrk "Cannot find a well-typed generalization of the goal that makes the proof progress.") - | NothingToRewrite -> - tclZEROMSG - (strbrk "Nothing to rewrite.") | e -> Proofview.tclZERO ~info e end diff --git a/tactics/equality.mli b/tactics/equality.mli index 90d8a224b..3e13ee570 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -11,7 +11,6 @@ open Names open Term open Evd open Environ -open Tacmach open Tacexpr open Ind_tables open Locus diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli index 42d00e1e1..2c4df0608 100644 --- a/tactics/evar_tactics.mli +++ b/tactics/evar_tactics.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Tacmach open Names open Tacexpr open Locus diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index c200871ef..27d25056e 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -8,7 +8,6 @@ open Names open Term -open Evd open Coqlib (** High-order patterns *) @@ -145,8 +144,6 @@ val is_matching_sigma : constr -> bool val match_eqdec : constr -> bool * constr * constr * constr * constr (** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *) -open Proof_type -open Tacmach val dest_nf_eq : [ `NF ] Proofview.Goal.t -> constr -> (constr * constr * constr) (** Match a negation *) diff --git a/tactics/inv.mli b/tactics/inv.mli index b3478dda2..412f30c20 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Loc open Names open Term open Misctypes diff --git a/tactics/leminv.mli b/tactics/leminv.mli index 47a4de444..2f80d26fc 100644 --- a/tactics/leminv.mli +++ b/tactics/leminv.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Loc open Names open Term open Constrexpr diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index cb20fc930..84c0a99b1 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -71,7 +71,6 @@ let interp_ml_tactic s = (* Summary and Object declaration *) open Nametab -open Libnames open Libobject let mactab = @@ -84,7 +83,6 @@ let is_ltac_for_ml_tactic r = fst (KNmap.find r !mactab) (* Declaration of the TAC-DEFINITION object *) let add (kn,td) = mactab := KNmap.add kn td !mactab -let replace (kn,td) = mactab := KNmap.add kn td !mactab let load_md i ((sp, kn), (local, id, b, t)) = match id with | None -> diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 59cd065d1..42e61cb57 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -100,20 +100,11 @@ let subst_evaluable subst = let subst_eval_ref = subst_evaluable_reference subst in subst_or_var (subst_and_short_name subst_eval_ref) -let subst_unfold subst (l,e) = - (l,subst_evaluable subst e) - -let subst_flag subst red = - { red with rConst = List.map (subst_evaluable subst) red.rConst } - let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c) let subst_glob_constr_or_pattern subst (c,p) = (subst_glob_constr subst c,subst_pattern subst p) -let subst_pattern_with_occurrences subst (l,p) = - (l,subst_glob_constr_or_pattern subst p) - let subst_redexp subst = Miscops.map_red_expr_gen (subst_glob_constr subst) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index cf2126f8d..61bef41d7 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -16,7 +16,6 @@ open Context open Declarations open Tacmach open Clenv -open Misctypes (************************************************************************) (* Tacticals re-exported from the Refiner module *) diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 6249bbc59..03ea89ad5 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -6,14 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Loc open Pp open Names open Term open Context open Tacmach open Proof_type -open Clenv open Tacexpr open Locus open Misctypes diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 07969c7d7..6f4c94e3f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -765,8 +765,6 @@ let intro = intro_gen (NamingAvoid []) MoveLast false false let introf = intro_gen (NamingAvoid []) MoveLast true false let intro_avoiding l = intro_gen (NamingAvoid l) MoveLast false false -let intro_then_force = intro_then_gen (NamingAvoid []) MoveLast true false - let intro_move_avoid idopt avoid hto = match idopt with | None -> intro_gen (NamingAvoid avoid) hto true false | Some id -> intro_gen (NamingMustBe (dloc,id)) hto true false @@ -2790,12 +2788,6 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = atomize_one (List.length argl) [] [] end -let find_atomic_param_of_ind nparams indtyp = - let argl = snd (decompose_app indtyp) in - let params,args = List.chop nparams argl in - let test c = isVar c && not (List.exists (dependent c) params) in - List.map destVar (List.filter test args) - (* [cook_sign] builds the lists [beforetoclear] (preceding the ind. var.) and [aftertoclear] (coming after the ind. var.) of hyps that must be erased, the lists of hyps to be generalize [decldeps] on the diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli index 5dbd5379a..807872988 100644 --- a/toplevel/auto_ind_decl.mli +++ b/toplevel/auto_ind_decl.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term open Names open Ind_tables diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 22ea09c53..2df7c2273 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util open Pp open Errors open Indtypes diff --git a/toplevel/classes.mli b/toplevel/classes.mli index 0a351d3cc..cb88ae564 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -8,7 +8,6 @@ open Names open Context -open Evd open Environ open Constrexpr open Typeclasses diff --git a/toplevel/command.mli b/toplevel/command.mli index 1de47d38c..3a38e52ce 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -11,7 +11,6 @@ open Term open Entries open Libnames open Globnames -open Tacexpr open Vernacexpr open Constrexpr open Decl_kinds diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli index d39e18a48..40f124ca3 100644 --- a/toplevel/obligations.mli +++ b/toplevel/obligations.mli @@ -14,7 +14,6 @@ open Pp open Globnames open Vernacexpr open Decl_kinds -open Tacexpr (** Forward declaration. *) val declare_fix_ref : (?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t -> |