diff options
46 files changed, 10 insertions, 253 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 48c9ca47a..7fba83e66 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -708,25 +708,6 @@ let check_no_explicitation l = | (_, Some (loc, _)) :: _ -> user_err_loc (loc,"",str"Unexpected explicitation of the argument of an abbreviation.") -(* This code is taken from dumpglob, and should be shared with it *) -let feedback_global loc ref = - if !Flags.ide_slave || !Flags.print_emacs then - let remove_sections dir = - if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then - Libnames.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ()) - else - dir in - let sp = Nametab.path_of_global ref in - let lib_dp = Lib.library_part ref in - let ty = "" in - let mod_dp,id = Libnames.repr_path sp in - let mod_dp = remove_sections mod_dp in - let mod_dp_trunc = Libnames.drop_dirpath_prefix lib_dp mod_dp in - let filepath = Names.DirPath.to_string lib_dp in - let modpath = Names.DirPath.to_string mod_dp_trunc in - let ident = Names.Id.to_string id in - Pp.feedback (Interface.GlobRef (loc, filepath, modpath, ident, ty)) - let dump_extended_global loc = function | TrueGlobal ref -> (*feedback_global loc ref;*) Dumpglob.add_glob loc ref | SynDef sp -> Dumpglob.add_glob_kn loc sp diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index f0d1aca4d..9589c0656 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -38,7 +38,6 @@ module Deltamap = struct let find_mp mp map = MPmap.find mp (fst map) let find_kn kn map = KNmap.find kn (snd map) let mem_mp mp map = MPmap.mem mp (fst map) - let mem_kn kn map = KNmap.mem kn (snd map) let fold_kn f map i = KNmap.fold f (snd map) i let fold fmp fkn (mm,km) i = MPmap.fold fmp mm (KNmap.fold fkn km i) diff --git a/kernel/vars.mli b/kernel/vars.mli index a09265036..ef3381ab5 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -53,6 +53,7 @@ val substnl_decl : constr list -> int -> rel_declaration -> rel_declaration val substl_decl : constr list -> rel_declaration -> rel_declaration val subst1_decl : constr -> rel_declaration -> rel_declaration +val substnl_named_decl : constr list -> int -> named_declaration -> named_declaration val subst1_named_decl : constr -> named_declaration -> named_declaration val substl_named_decl : constr list -> named_declaration -> named_declaration diff --git a/lib/bigint.ml b/lib/bigint.ml index 4dc93e6e8..de096493f 100644 --- a/lib/bigint.ml +++ b/lib/bigint.ml @@ -63,7 +63,6 @@ module ArrayInt = struct (* Basic numbers *) let zero = [||] -let neg_one = [|-1|] let is_zero = function | [||] -> true @@ -74,7 +73,7 @@ let is_zero = function - it is [|-1|] - its first bloc is in [-base;-1[U]0;base[ and the other blocs are in [0;base[. *) - +(* let canonical n = let ok x = (0 <= x && x < base) in let rec ok_tail k = (Int.equal k 0) || (ok n.(k) && ok_tail (k-1)) in @@ -82,6 +81,7 @@ let canonical n = in (is_zero n) || (match n with [|-1|] -> true | _ -> false) || (ok_init n.(0) && ok_tail (Array.length n - 1)) +*) (* [normalize_pos] : removing initial blocks of 0 *) diff --git a/lib/util.ml b/lib/util.ml index c293e4dfd..9ade75147 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -100,10 +100,6 @@ let iterate = let repeat n f x = let rec loop i = if i <> 0 then (f x; loop (i - 1)) in loop n -let iterate_for a b f x = - let rec iterate i v = if i > b then v else iterate (succ i) (f i v) in - iterate a x - let app_opt f x = match f with | Some f -> f x diff --git a/lib/util.mli b/lib/util.mli index c9456802d..d3e3432a3 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -87,7 +87,6 @@ val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b val const : 'a -> 'b -> 'a val iterate : ('a -> 'a) -> int -> 'a -> 'a val repeat : int -> ('a -> unit) -> 'a -> unit -val iterate_for : int -> int -> (int -> 'a -> 'a) -> 'a -> 'a val app_opt : ('a -> 'a) option -> 'a -> 'a (** {6 Delayed computations. } *) diff --git a/library/global.ml b/library/global.ml index 9f683b2ff..a8121d15f 100644 --- a/library/global.ml +++ b/library/global.ml @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Term open Environ (** We introduce here the global environment of the system, diff --git a/library/globnames.mli b/library/globnames.mli index 0a7bf850c..5d717965e 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -49,12 +49,14 @@ val reference_of_constr : constr -> global_reference module RefOrdered : sig type t = global_reference val compare : t -> t -> int + val equal : t -> t -> bool val hash : t -> int end module RefOrdered_env : sig type t = global_reference val compare : t -> t -> int + val equal : t -> t -> bool val hash : t -> int end diff --git a/library/nametab.ml b/library/nametab.ml index 03856736d..1a30e80d1 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -15,14 +15,10 @@ open Globnames exception GlobalizationError of qualid -exception GlobalizationConstantError of qualid let error_global_not_found_loc loc q = Loc.raise loc (GlobalizationError q) -let error_global_constant_not_found_loc loc q = - Loc.raise loc (GlobalizationConstantError q) - let error_global_not_found q = raise (GlobalizationError q) (* Kinds of global names *) diff --git a/library/nametab.mli b/library/nametab.mli index 43c174f1b..d9038c774 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -58,12 +58,10 @@ open Globnames exception GlobalizationError of qualid -exception GlobalizationConstantError of qualid (** Raises a globalization error *) val error_global_not_found_loc : Loc.t -> qualid -> 'a val error_global_not_found : qualid -> 'a -val error_global_constant_not_found_loc : Loc.t -> qualid -> 'a (** {6 Register visibility of things } *) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 104f26641..a7957ebe8 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -37,8 +37,6 @@ type pattern_matching_error = | BadConstructor of constructor * inductive | WrongNumargConstructor of constructor * int | WrongNumargInductive of inductive * int - | WrongPredicateArity of constr * constr * constr - | NeedsInversion of constr * constr | UnusedClause of cases_pattern list | NonExhaustive of cases_pattern list | CannotInferPredicate of (constr * types) array @@ -60,12 +58,6 @@ let error_wrong_numarg_constructor_loc loc env c n = let error_wrong_numarg_inductive_loc loc env c n = raise_pattern_matching_error (loc, env, WrongNumargInductive(c,n)) -let error_wrong_predicate_arity_loc loc env c n1 n2 = - raise_pattern_matching_error (loc, env, WrongPredicateArity (c,n1,n2)) - -let error_needs_inversion env x t = - raise (PatternMatchingError (env, NeedsInversion (x,t))) - let rec list_try_compile f = function | [a] -> f a | [] -> anomaly (str "try_find_f") diff --git a/pretyping/cases.mli b/pretyping/cases.mli index b5bb27da9..70fa945ff 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -23,28 +23,16 @@ type pattern_matching_error = | BadConstructor of constructor * inductive | WrongNumargConstructor of constructor * int | WrongNumargInductive of inductive * int - | WrongPredicateArity of constr * constr * constr - | NeedsInversion of constr * constr | UnusedClause of cases_pattern list | NonExhaustive of cases_pattern list | CannotInferPredicate of (constr * types) array exception PatternMatchingError of env * pattern_matching_error -val raise_pattern_matching_error : (Loc.t * env * pattern_matching_error) -> 'a - val error_wrong_numarg_constructor_loc : Loc.t -> env -> constructor -> int -> 'a val error_wrong_numarg_inductive_loc : Loc.t -> env -> inductive -> int -> 'a -val error_bad_constructor_loc : Loc.t -> constructor -> inductive -> 'a - -val error_bad_pattern_loc : Loc.t -> constructor -> constr -> 'a - -val error_wrong_predicate_arity_loc : Loc.t -> env -> constr -> constr -> constr -> 'a - -val error_needs_inversion : env -> constr -> types -> 'a - (** {6 Compilation primitive. } *) val compile_cases : diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 170e21a90..c66ca7ac1 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -221,9 +221,6 @@ let get_type_of ?(polyprop=true) ?(refresh=true) ?(lax=false) env sigma c = let t = if lax then f env c else anomaly_on_error (f env) c in if refresh then refresh_universes t else t -(* Makes an assumption from a constr *) -let get_assumption_of env evc c = c - (* Makes an unsafe judgment from a constr *) let get_judgment_of env evc c = { uj_val = c; uj_type = get_type_of env evc c } diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index bb3ffa411..c2a08f4b9 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -35,9 +35,6 @@ val get_sort_of : val get_sort_family_of : ?polyprop:bool -> env -> evar_map -> types -> sorts_family -(** Makes an assumption from a constr *) -val get_assumption_of : env -> evar_map -> constr -> types - (** Makes an unsafe judgment from a constr *) val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment diff --git a/pretyping/unification.ml b/pretyping/unification.ml index fbb7de7af..bfcc469c5 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1004,7 +1004,6 @@ let w_unify_core_0 env evd with_types cv_pb flags m n = let evd = w_merge env with_types flags subst2 in try_resolve_typeclasses env evd flags m n -let w_unify_0 env evd = w_unify_core_0 env evd false let w_typed_unify env evd = w_unify_core_0 env evd true let w_typed_unify_array env evd flags f1 l1 f2 l2 = diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 5dd4587a0..04e65b862 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -60,8 +60,6 @@ val w_coerce_to_type : env -> evar_map -> constr -> types -> types -> (exported for inv.ml) *) val abstract_list_all : env -> evar_map -> constr -> constr -> constr list -> constr * types -val abstract_list_all_with_dependencies : - env -> evar_map -> types -> constr -> constr list -> constr (* For tracing *) diff --git a/printing/printer.ml b/printing/printer.ml index b16c8c502..4bab893d7 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -648,9 +648,6 @@ let pr_prim_rule = function (str (if withdep then "dependent " else "") ++ str"move " ++ pr_id id1 ++ Miscprint.pr_move_location pr_id id2) - | Order ord -> - (str"order " ++ pr_sequence pr_id ord) - | Rename (id1,id2) -> (str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2) diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 444043dbe..64a9f0024 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -23,7 +23,6 @@ open Tacred open Pretype_errors open Evarutil open Unification -open Mod_subst open Misctypes (* Abbreviations *) @@ -43,12 +42,6 @@ type clausenv = { let cl_env ce = ce.env let cl_sigma ce = ce.evd -let subst_clenv sub clenv = - { templval = map_fl (subst_mps sub) clenv.templval; - templtyp = map_fl (subst_mps sub) clenv.templtyp; - evd = subst_evar_defs_light sub clenv.evd; - env = clenv.env } - let clenv_nf_meta clenv c = nf_meta clenv.evd c let clenv_term clenv c = meta_instance clenv.evd c let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv @@ -304,8 +297,6 @@ let clenv_pose_metas_as_evars clenv dep_mvs = fold clenv mvs in fold clenv dep_mvs -let evar_clenv_unique_resolver = clenv_unique_resolver - (******************************************************************) let connect_clenv gls clenv = diff --git a/proofs/clenv.mli b/proofs/clenv.mli index e74c4875f..ab4f3af79 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -23,11 +23,6 @@ type clausenv = { out *) templtyp : constr freelisted (** its type *)} -(** Substitution is not applied on templenv (because [subst_clenv] is - applied only on hints which typing env is overwritten by the - goal env) *) -val subst_clenv : substitution -> clausenv -> clausenv - (** subject of clenv (instantiated) *) val clenv_value : clausenv -> constr @@ -62,11 +57,6 @@ val clenv_unify : val clenv_unique_resolver : ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv -(** same as above ([allow_K=false]) but replaces remaining metas - with fresh evars if [evars_flag] is [true] *) -val evar_clenv_unique_resolver : - ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv - val clenv_dependent : clausenv -> metavariable list val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index c0036d192..7a1a14bde 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -79,9 +79,6 @@ let dft = default_unify_flags let res_pf clenv ?(with_evars=false) ?(flags=dft) gls = clenv_refine with_evars (clenv_unique_resolver ~flags clenv gls) gls -let e_res_pf clenv = res_pf clenv ~with_evars:true ~flags:dft - - (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en particulier ne semblent pas vérifier que des instances différentes d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index f635012fe..173eb32e3 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -19,6 +19,3 @@ val res_pf : clausenv -> ?with_evars:evars_flag -> ?flags:unify_flags -> tactic val clenv_pose_dependent_evars : evars_flag -> clausenv -> clausenv val clenv_value_cast_meta : clausenv -> constr - -(** Compatibility, use res_pf ?with_evars:true instead *) -val e_res_pf : clausenv -> tactic diff --git a/proofs/logic.ml b/proofs/logic.ml index 30905e577..054e6db6c 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -695,12 +695,6 @@ let prim_refiner r sigma goal = let sigma = Goal.V82.partial_solution sigma goal ev in ([gl], sigma) - | Order ord -> - let hyps' = reorder_val_context env sign ord in - let (gl,ev,sigma) = mk_goal hyps' cl in - let sigma = Goal.V82.partial_solution sigma goal ev in - ([gl], sigma) - | Rename (id1,id2) -> if !check && not (Id.equal id1 id2) && Id.List.mem id2 diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index f98bfa5ea..7297706e1 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -37,7 +37,6 @@ type prim_rule = | Thin of Id.t list | ThinBody of Id.t list | Move of bool * Id.t * Id.t move_location - | Order of Id.t list | Rename of Id.t * Id.t (** Nowadays, the only rules we'll consider are the primitive rules *) diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index a5d694077..0aadd862b 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -29,7 +29,6 @@ type prim_rule = | Thin of Id.t list | ThinBody of Id.t list | Move of bool * Id.t * Id.t move_location - | Order of Id.t list | Rename of Id.t * Id.t (** Nowadays, the only rules we'll consider are the primitive rules *) diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 2ea877725..f73bdaf93 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -65,10 +65,6 @@ val tclTHENSV : tactic -> tactic array -> tactic (** Same with a list of tactics *) val tclTHENS : tactic -> tactic list -> tactic -(** [tclTHENST] is renamed [tclTHENSFIRSTn] -val tclTHENST : tactic -> tactic array -> tactic -> tactic -*) - (** [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls] applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m] diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 0f898feef..a36b7f2ac 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -71,8 +71,6 @@ let pf_get_new_ids ids gls = let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id -let pf_parse_const gls = compose (pf_global gls) Id.of_string - let pf_reduction_of_red_expr gls re c = (fst (reduction_of_red_expr (pf_env gls) re)) (pf_env gls) (project gls) c @@ -80,9 +78,7 @@ let pf_apply f gls = f (pf_env gls) (project gls) let pf_reduce = pf_apply let pf_whd_betadeltaiota = pf_reduce whd_betadeltaiota -let pf_whd_betadeltaiota_stack = pf_reduce whd_betadeltaiota_stack let pf_hnf_constr = pf_reduce hnf_constr -let pf_red_product = pf_reduce red_product let pf_nf = pf_reduce simpl let pf_nf_betaiota = pf_reduce (fun _ -> nf_betaiota) let pf_compute = pf_reduce compute @@ -92,15 +88,11 @@ let pf_get_type_of = pf_reduce Retyping.get_type_of let pf_conv_x = pf_reduce is_conv let pf_conv_x_leq = pf_reduce is_conv_leq -let pf_const_value = pf_reduce (fun env _ -> constant_value env) let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind let pf_hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls) -let pf_check_type gls c1 c2 = - ignore (pf_type_of gls (mkCast (c1, DEFAULTcast, c2))) - let pf_is_matching = pf_apply ConstrMatching.is_matching_conv let pf_matches = pf_apply ConstrMatching.matches_conv @@ -140,9 +132,6 @@ let thin_body_no_check ids gl = let move_hyp_no_check with_dep id1 id2 gl = refiner (Move (with_dep,id1,id2)) gl -let order_hyps idl gl = - refiner (Order idl) gl - let rec rename_hyp_no_check l gl = match l with | [] -> tclIDTAC gl | (id1,id2)::l -> diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 6e4890807..92f8ef829 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -41,9 +41,7 @@ val pf_nth_hyp_id : goal sigma -> int -> Id.t val pf_last_hyp : goal sigma -> named_declaration val pf_ids_of_hyps : goal sigma -> Id.t list val pf_global : goal sigma -> Id.t -> constr -val pf_parse_const : goal sigma -> string -> constr val pf_type_of : goal sigma -> constr -> types -val pf_check_type : goal sigma -> constr -> types -> unit val pf_hnf_type_of : goal sigma -> constr -> types val pf_get_hyp : goal sigma -> Id.t -> named_declaration @@ -61,9 +59,7 @@ val pf_reduce : goal sigma -> constr -> constr val pf_whd_betadeltaiota : goal sigma -> constr -> constr -val pf_whd_betadeltaiota_stack : goal sigma -> constr -> constr * constr list val pf_hnf_constr : goal sigma -> constr -> constr -val pf_red_product : goal sigma -> constr -> constr val pf_nf : goal sigma -> constr -> constr val pf_nf_betaiota : goal sigma -> constr -> constr val pf_reduce_to_quantified_ind : goal sigma -> types -> inductive * types @@ -72,7 +68,6 @@ val pf_compute : goal sigma -> constr -> constr val pf_unfoldn : (occurrences * evaluable_global_reference) list -> goal sigma -> constr -> constr -val pf_const_value : goal sigma -> constant -> constr val pf_conv_x : goal sigma -> constr -> constr -> bool val pf_conv_x_leq : goal sigma -> constr -> constr -> bool @@ -85,16 +80,10 @@ val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool val refiner : rule -> tactic val introduction_no_check : Id.t -> tactic val internal_cut_no_check : bool -> Id.t -> types -> tactic -val internal_cut_rev_no_check : bool -> Id.t -> types -> tactic val refine_no_check : constr -> tactic val convert_concl_no_check : types -> cast_kind -> tactic val convert_hyp_no_check : named_declaration -> tactic val thin_no_check : Id.t list -> tactic -val thin_body_no_check : Id.t list -> tactic -val move_hyp_no_check : - bool -> Id.t -> Id.t move_location -> tactic -val rename_hyp_no_check : (Id.t*Id.t) list -> tactic -val order_hyps : Id.t list -> tactic val mutual_fix : Id.t -> int -> (Id.t * int * constr) list -> int -> tactic val mutual_cofix : Id.t -> (Id.t * constr) list -> int -> tactic @@ -125,7 +114,6 @@ module New : sig val pf_env : 'a Proofview.Goal.t -> Environ.env val pf_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types - val pf_get_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types val pf_conv_x : 'a Proofview.Goal.t -> Term.constr -> Term.constr -> bool val pf_get_new_id : identifier -> [ `NF ] Proofview.Goal.t -> identifier diff --git a/tactics/dn.mli b/tactics/dn.mli index 78896ae9a..20407e9d9 100644 --- a/tactics/dn.mli +++ b/tactics/dn.mli @@ -36,6 +36,4 @@ sig val app : (Z.t -> unit) -> t -> unit - val skip_arg : int -> t -> (t * bool) list - end diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 6c3c55efd..0ab426cd2 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -58,8 +58,6 @@ let registered_e_assumption gl = (*s Tactics handling a list of goals. *) -type tactic_list = (goal list sigma) -> (goal list sigma) - (* first_goal : goal list sigma -> goal sigma *) let first_goal gls = @@ -201,10 +199,6 @@ module SearchProblem = struct let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl) - let pr_goals gls = - let evars = Evarutil.nf_evar_map (Refiner.project gls) in - prlist (pr_ev evars) (sig_it gls) - let filter_tactics glls l = (* let _ = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *) (* let evars = Evarutil.nf_evars (Refiner.project glls) in *) @@ -489,8 +483,6 @@ let autounfold_tac db cls gl = in autounfold dbs cls gl -open Extraargs - TACTIC EXTEND autounfold | [ "autounfold" hintbases(db) clause(cl) ] -> [ Proofview.V82.tactic (autounfold_tac db cl) ] END diff --git a/tactics/elim.ml b/tactics/elim.ml index 845c4eee1..0720273bb 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -113,11 +113,6 @@ let decompose_these c l = general_decompose (fun (_,t) -> head_in indl t gl) c end -let decompose_nonrec c = - general_decompose - (fun (_,t) -> is_non_recursive_type t) - c - let decompose_and c = general_decompose (fun (_,t) -> is_record t) diff --git a/tactics/elim.mli b/tactics/elim.mli index b83a97bcc..b5e89de08 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -13,20 +13,11 @@ open Misctypes (** Eliminations tactics. *) -val introElimAssumsThen : - (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic - val introCaseAssumsThen : (intro_pattern_expr Loc.located list -> branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic -val general_decompose : (Id.t * constr -> bool) -> constr -> unit Proofview.tactic -val decompose_nonrec : constr -> unit Proofview.tactic -val decompose_and : constr -> unit Proofview.tactic -val decompose_or : constr -> unit Proofview.tactic val h_decompose : inductive list -> constr -> unit Proofview.tactic val h_decompose_or : constr -> unit Proofview.tactic val h_decompose_and : constr -> unit Proofview.tactic - -val double_ind : quantified_hypothesis -> quantified_hypothesis -> unit Proofview.tactic val h_double_induction : quantified_hypothesis -> quantified_hypothesis-> unit Proofview.tactic diff --git a/tactics/equality.ml b/tactics/equality.ml index a480f6de6..71b3c0045 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -563,12 +563,8 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt = let replace c2 c1 = multi_replace onConcl c2 c1 false None -let replace_in id c2 c1 = multi_replace (onHyp id) c2 c1 false None - let replace_by c2 c1 tac = multi_replace onConcl c2 c1 false (Some tac) -let replace_in_by id c2 c1 tac = multi_replace (onHyp id) c2 c1 false (Some tac) - let replace_in_clause_maybe_by c2 c1 cl tac_opt = multi_replace cl c2 c1 false tac_opt diff --git a/tactics/equality.mli b/tactics/equality.mli index 5ea0f9333..b59b4bbe0 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -69,13 +69,10 @@ val general_multi_multi_rewrite : val replace_in_clause_maybe_by : constr -> constr -> clause -> unit Proofview.tactic option -> unit Proofview.tactic val replace : constr -> constr -> unit Proofview.tactic -val replace_in : Id.t -> constr -> constr -> unit Proofview.tactic val replace_by : constr -> constr -> unit Proofview.tactic -> unit Proofview.tactic -val replace_in_by : Id.t -> constr -> constr -> unit Proofview.tactic -> unit Proofview.tactic val discr : evars_flag -> constr with_bindings -> unit Proofview.tactic val discrConcl : unit Proofview.tactic -val discrClause : evars_flag -> clause -> unit Proofview.tactic val discrHyp : Id.t -> unit Proofview.tactic val discrEverywhere : evars_flag -> unit Proofview.tactic val discr_tac : evars_flag -> @@ -101,9 +98,6 @@ val cutRewriteInConcl : bool -> constr -> unit Proofview.tactic val rewriteInHyp : bool -> constr -> Id.t -> unit Proofview.tactic val rewriteInConcl : bool -> constr -> unit Proofview.tactic -(* Expect the proof of an equality; fails with raw internal errors *) -val substClause : bool -> constr -> Id.t option -> unit Proofview.tactic - val discriminable : env -> evar_map -> constr -> constr -> bool val injectable : env -> evar_map -> constr -> constr -> bool diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index 6cc0af2c6..89aaee485 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -18,6 +18,7 @@ open Inductiveops open ConstrMatching open Coqlib open Declarations +open Tacmach.New (* I implemented the following functions which test whether a term t is an inductive but non-recursive type, a general conjuction, a @@ -396,10 +397,10 @@ let find_eq_data eqn = (* fails with PatternMatchingFailure *) let extract_eq_args gl = function | MonomorphicLeibnizEq (e1,e2) -> - let t = Tacmach.New.pf_type_of gl e1 in (t,e1,e2) + let t = pf_type_of gl e1 in (t,e1,e2) | PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2) | HeterogenousEq (t1,e1,t2,e2) -> - if Tacmach.New.pf_conv_x gl t1 t2 then (t1,e1,e2) + if pf_conv_x gl t1 t2 then (t1,e1,e2) else raise PatternMatchingFailure let find_eq_data_decompose gl eqn = @@ -418,13 +419,11 @@ let find_this_eq_data_decompose gl eqn = error "Don't know what to do with JMeq on arguments not of same type." in (lbeq,eq_args) -open Tacmach - let match_eq_nf gls eqn eq_pat = - match Id.Map.bindings (Tacmach.New.pf_matches gls (Lazy.force eq_pat) eqn) with + match Id.Map.bindings (pf_matches gls (Lazy.force eq_pat) eqn) with | [(m1,t);(m2,x);(m3,y)] -> assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3); - (t,Tacmach.New.pf_whd_betadeltaiota gls x,Tacmach.New.pf_whd_betadeltaiota gls y) + (t,pf_whd_betadeltaiota gls x,pf_whd_betadeltaiota gls y) | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 terms") let dest_nf_eq gls eqn = diff --git a/tactics/inv.ml b/tactics/inv.ml index 5667e7015..acd959e1d 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -21,7 +21,6 @@ open Inductiveops open Printer open Retyping open Tacmach.New -open Clenv open Tacticals.New open Tactics open Elim @@ -32,24 +31,6 @@ open Proofview.Notations let clear hyps = Proofview.V82.tactic (clear hyps) -let collect_meta_variables c = - let rec collrec acc c = match kind_of_term c with - | Meta mv -> mv::acc - | _ -> fold_constr collrec acc c - in - collrec [] c - -let check_no_metas clenv ccl = - if occur_meta ccl then - let metas = List.filter (fun m -> not (Evd.meta_defined clenv.evd m)) - (collect_meta_variables ccl) in - let metas = List.map (Evd.meta_name clenv.evd) metas in - let opts = match metas with [_] -> " " | _ -> "s " in - errorlabstrm "inversion" - (str ("Cannot find an instantiation for variable"^opts) ++ - prlist_with_sep pr_comma pr_name metas - (* ajouter "in " ++ pr_lconstr ccl mais il faut le bon contexte *)) - let var_occurs_in_pf gl id = let env = Proofview.Goal.env gl in occur_var env id (Proofview.Goal.concl gl) || @@ -518,13 +499,11 @@ open Tacexpr let inv k = inv_gen false k NoDep -let half_inv_tac id = inv SimpleInversion None (NamedHyp id) let inv_tac id = inv FullInversion None (NamedHyp id) let inv_clear_tac id = inv FullInversionClear None (NamedHyp id) let dinv k c = inv_gen false k (Dep c) -let half_dinv_tac id = dinv SimpleInversion None None (NamedHyp id) let dinv_tac id = dinv FullInversion None None (NamedHyp id) let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id) diff --git a/tactics/inv.mli b/tactics/inv.mli index f5820c33c..615ceaab5 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -14,13 +14,6 @@ open Tacexpr type inversion_status = Dep of constr option | NoDep -val inv_gen : - bool -> inversion_kind -> inversion_status -> - intro_pattern_expr located option -> quantified_hypothesis -> unit Proofview.tactic -val invIn_gen : - inversion_kind -> intro_pattern_expr located option -> Id.t list -> - quantified_hypothesis -> unit Proofview.tactic - val inv_clause : inversion_kind -> intro_pattern_expr located option -> Id.t list -> quantified_hypothesis -> unit Proofview.tactic @@ -31,9 +24,7 @@ val inv : inversion_kind -> intro_pattern_expr located option -> val dinv : inversion_kind -> constr option -> intro_pattern_expr located option -> quantified_hypothesis -> unit Proofview.tactic -val half_inv_tac : Id.t -> unit Proofview.tactic val inv_tac : Id.t -> unit Proofview.tactic val inv_clear_tac : Id.t -> unit Proofview.tactic -val half_dinv_tac : Id.t -> unit Proofview.tactic val dinv_tac : Id.t -> unit Proofview.tactic val dinv_clear_tac : Id.t -> unit Proofview.tactic diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 2e55869de..5e5de2589 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -22,7 +22,6 @@ open Entries open Inductiveops open Environ open Tacmach.New -open Pfedit open Clenv open Declare open Tacticals.New diff --git a/tactics/leminv.mli b/tactics/leminv.mli index 76223abed..6d8d07da6 100644 --- a/tactics/leminv.mli +++ b/tactics/leminv.mli @@ -12,9 +12,6 @@ open Term open Constrexpr open Misctypes -val lemInv_gen : quantified_hypothesis -> constr -> unit Proofview.tactic -val lemInvIn_gen : quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic - val lemInv_clause : quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index f1b52ebc7..bd33e5146 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -63,13 +63,6 @@ let tclIFTHENTRYELSEMUST = Refiner.tclIFTHENTRYELSEMUST let tclTHENSEQ = tclTHENLIST -(* Experimental *) - -let rec tclFIRST_PROGRESS_ON tac = function - | [] -> tclFAIL 0 (str "No applicable tactic") - | [a] -> tac a (* so that returned failure is the one from last item *) - | a::tl -> tclORELSE (tac a) (tclFIRST_PROGRESS_ON tac tl) - (************************************************************************) (* Tacticals applying on hypotheses *) (************************************************************************) @@ -126,9 +119,6 @@ let fullGoal gl = None :: List.map Option.make (pf_ids_of_hyps gl) let onAllHyps tac gl = tclMAP tac (pf_ids_of_hyps gl) gl let onAllHypsAndConcl tac gl = tclMAP tac (fullGoal gl) gl -let tryAllHyps tac gl = tclFIRST_PROGRESS_ON tac (pf_ids_of_hyps gl) gl -let tryAllHypsAndConcl tac gl = tclFIRST_PROGRESS_ON tac (fullGoal gl) gl - let onClause tac cl gls = let hyps () = pf_ids_of_hyps gls in tclMAP tac (Locusops.simple_clause_of hyps cl) gls diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 2944ff690..fcc23df22 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -58,8 +58,6 @@ val tclIFTHENSELSE : tactic -> tactic list -> tactic -> tactic val tclIFTHENSVELSE : tactic -> tactic array -> tactic -> tactic val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic -val tclFIRST_PROGRESS_ON : ('a -> tactic) -> 'a list -> tactic - (** {6 Tacticals applying to hypotheses } *) val onNthHypId : int -> (Id.t -> tactic) -> tactic @@ -94,9 +92,6 @@ val onHyps : (goal sigma -> named_context) -> goal; in particular, it can abstractly refer to the set of hypotheses independently of the effective contents of the current goal *) -val tryAllHyps : (Id.t -> tactic) -> tactic -val tryAllHypsAndConcl : (Id.t option -> tactic) -> tactic - val onAllHyps : (Id.t -> tactic) -> tactic val onAllHypsAndConcl : (Id.t option -> tactic) -> tactic @@ -200,7 +195,6 @@ module New : sig val tclTRY : unit tactic -> unit tactic val tclFIRST : unit tactic list -> unit tactic - val tclFIRST_PROGRESS_ON : ('a -> unit tactic) -> 'a list -> unit tactic val tclIFTHENELSE : unit tactic -> unit tactic -> unit tactic -> unit tactic val tclIFTHENSVELSE : unit tactic -> unit tactic array -> unit tactic -> unit tactic val tclIFTHENTRYELSEMUST : unit tactic -> unit tactic -> unit tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index be5b0de3a..ab1af8c3e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -490,8 +490,6 @@ let rec intros_using = function let intros = Tacticals.New.tclREPEAT intro -let intro_erasing id = tclTHEN (thin [id]) (introduction id) - let intro_forthcoming_then_gen loc name_flag move_flag dep_flag tac = let rec aux ids = Proofview.tclORELSE @@ -932,9 +930,6 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags) id i elimclause (str "Nothing to rewrite in " ++ pr_id id ++ str"."); clenv_refine_in with_evars id elimclause'' gl -let general_elim_in with_evars id = - general_elim_clause (elimination_in_clause_scheme with_evars id) - (* Apply a tactic below the products of the conclusion of a lemma *) type conjunction_status = diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 0e92e7eb9..5b7ad1f88 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -64,7 +64,6 @@ val intro_using : Id.t -> unit Proofview.tactic val intro_mustbe_force : Id.t -> unit Proofview.tactic val intro_then : (Id.t -> unit Proofview.tactic) -> unit Proofview.tactic val intros_using : Id.t list -> unit Proofview.tactic -val intro_erasing : Id.t -> tactic val intros_replacing : Id.t list -> unit Proofview.tactic val intros : unit Proofview.tactic @@ -256,8 +255,6 @@ val general_elim_clause_gen : (int -> Clenv.clausenv -> 'a -> tactic) -> val general_elim : evars_flag -> constr with_bindings -> eliminator -> tactic -val general_elim_in : evars_flag -> Id.t -> - constr with_bindings -> eliminator -> tactic val default_elim : evars_flag -> constr with_bindings -> unit Proofview.tactic val simplest_elim : constr -> unit Proofview.tactic @@ -328,7 +325,6 @@ val setoid_symmetry : unit Proofview.tactic Hook.t val symmetry_red : bool -> unit Proofview.tactic val symmetry : unit Proofview.tactic val setoid_symmetry_in : (Id.t -> unit Proofview.tactic) Hook.t -val symmetry_in : Id.t -> unit Proofview.tactic val intros_symmetry : clause -> unit Proofview.tactic val setoid_transitivity : (constr option -> unit Proofview.tactic) Hook.t diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 10c3092b4..0186b08ac 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -102,10 +102,6 @@ let process_vernac_interp_error exn = match exn with (str "The reference" ++ spc () ++ Libnames.pr_qualid q ++ spc () ++ str "was not found" ++ spc () ++ str "in the current" ++ spc () ++ str "environment.") - | Nametab.GlobalizationConstantError q -> - wrap_vernac_error exn - (str "No constant of this name:" ++ spc () ++ - Libnames.pr_qualid q ++ str ".") | Refiner.FailError (i,s) -> let s = Lazy.force s in wrap_vernac_error exn diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 954d75493..51dc8d5bb 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -73,8 +73,6 @@ let outputstate = ref "" let set_outputstate s = outputstate:=s let outputstate () = if not (String.is_empty !outputstate) then extern_state !outputstate -let set_default_include d = - push_include d Nameops.default_root_prefix false false let set_include d p recursive implicit = let p = dirpath_of_string p in push_include d p recursive implicit diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index b2f752dce..fd74f9c06 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1064,23 +1064,6 @@ let explain_wrong_numarg_inductive env ind n = str "The inductive type " ++ pr_inductive env ind ++ str " expects " ++ str (decline_string n "argument") ++ str "." -let explain_wrong_predicate_arity env pred nondep_arity dep_arity= - let env = make_all_name_different env in - let pp = pr_lconstr_env env pred in - str "The elimination predicate " ++ spc () ++ pp ++ fnl () ++ - str "should be of arity" ++ spc () ++ - pr_lconstr_env env nondep_arity ++ spc () ++ - str "(for non dependent case) or" ++ - spc () ++ pr_lconstr_env env dep_arity ++ spc () ++ - str "(for dependent case)." - -let explain_needs_inversion env x t = - let env = make_all_name_different env in - let px = pr_lconstr_env env x in - let pt = pr_lconstr_env env t in - str "Sorry, I need inversion to compile pattern matching on term " ++ - px ++ str " of type: " ++ pt ++ str "." - let explain_unused_clause env pats = (* Without localisation let s = if List.length pats > 1 then "s" else "" in @@ -1112,10 +1095,6 @@ let explain_pattern_matching_error env = function explain_wrong_numarg_constructor env c n | WrongNumargInductive (c,n) -> explain_wrong_numarg_inductive env c n - | WrongPredicateArity (pred,n,dep) -> - explain_wrong_predicate_arity env pred n dep - | NeedsInversion (x,t) -> - explain_needs_inversion env x t | UnusedClause tms -> explain_unused_clause env tms | NonExhaustive tms -> diff --git a/toplevel/stm.ml b/toplevel/stm.ml index fc52d3644..875c933ef 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -332,7 +332,6 @@ end = struct (* {{{ *) let current_branch () = current_branch !vcs let checkout head = vcs := checkout !vcs head - let master = Branch.master let branches () = branches !vcs let get_branch head = get_branch !vcs head let get_branch_pos head = (get_branch head).pos |