aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml7
-rw-r--r--tactics/autorewrite.ml4
-rw-r--r--tactics/btermdn.ml2
-rw-r--r--tactics/class_tactics.ml14
-rw-r--r--tactics/eauto.ml9
-rw-r--r--tactics/elimschemes.ml4
-rw-r--r--tactics/eqschemes.ml34
-rw-r--r--tactics/equality.ml53
-rw-r--r--tactics/equality.mli10
-rw-r--r--tactics/hints.ml76
-rw-r--r--tactics/hints.mli39
-rw-r--r--tactics/hipattern.ml6
-rw-r--r--tactics/hipattern.mli2
-rw-r--r--tactics/ind_tables.ml4
-rw-r--r--tactics/inv.ml12
-rw-r--r--tactics/inv.mli5
-rw-r--r--tactics/tacticals.ml46
-rw-r--r--tactics/tacticals.mli8
-rw-r--r--tactics/tactics.ml163
-rw-r--r--tactics/tactics.mli17
-rw-r--r--tactics/term_dnet.ml2
21 files changed, 295 insertions, 222 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 0c0d9bcfc4..77fe314150 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -8,8 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-module CVars = Vars
-
open Pp
open Util
open Names
@@ -81,15 +79,14 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl =
let clenv, c =
if poly then
(** Refresh the instance of the hint *)
- let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in
- let map c = CVars.subst_univs_level_constr subst c in
+ let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
let emap c = Vars.subst_univs_level_constr subst c in
let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
(** Only metas are mentioning the old universes. *)
let clenv = {
templval = Evd.map_fl emap clenv.templval;
templtyp = Evd.map_fl emap clenv.templtyp;
- evd = Evd.map_metas map evd;
+ evd = Evd.map_metas emap evd;
env = Proofview.Goal.env gl;
} in
clenv, emap c
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index c3857e6b8b..0b0e629ab5 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -30,7 +30,7 @@ let subst_hint subst hint =
let cst' = subst_mps subst hint.rew_lemma in
let typ' = subst_mps subst hint.rew_type in
let pat' = subst_mps subst hint.rew_pat in
- let t' = Option.smartmap (Genintern.generic_substitute subst) hint.rew_tac in
+ let t' = Option.Smart.map (Genintern.generic_substitute subst) hint.rew_tac in
if hint.rew_lemma == cst' && hint.rew_type == typ' && hint.rew_tac == t' then hint else
{ hint with
rew_lemma = cst'; rew_type = typ';
@@ -93,7 +93,7 @@ let one_base general_rewrite_maybe_in tac_main bas =
let try_rewrite dir ctx c tc =
Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
- let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in
+ let subst, ctx' = UnivGen.fresh_universe_context_set_instance ctx in
let c' = Vars.subst_univs_level_constr subst c in
let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx' in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 8e50c977e7..8f50b0aa23 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -22,7 +22,7 @@ open Globnames
let dnet_depth = ref 8
type term_label =
-| GRLabel of global_reference
+| GRLabel of GlobRef.t
| ProdLabel
| LambdaLabel
| SortLabel
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 0260460e64..3e08c6d878 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -226,7 +226,7 @@ let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) =
Refine.refine ~typecheck:false begin fun sigma ->
let sigma, term, ty =
if poly then
- let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in
+ let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
let map c = Vars.subst_univs_level_constr subst c in
let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
sigma, map c, map t
@@ -547,9 +547,9 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
(List.map_append
(fun (path,info,c) ->
let info =
- { info with Vernacexpr.hint_pattern =
+ { info with hint_pattern =
Option.map (Constrintern.intern_constr_pattern env sigma)
- info.Vernacexpr.hint_pattern }
+ info.hint_pattern }
in
make_resolves env sigma ~name:(PathHints path)
(true,false,not !Flags.quiet) info false
@@ -1030,8 +1030,8 @@ module Intpart = Unionfind.Make(Evar.Set)(Evar.Map)
let deps_of_constraints cstrs evm p =
List.iter (fun (_, _, x, y) ->
- let evx = Evarutil.undefined_evars_of_term evm (EConstr.of_constr x) in
- let evy = Evarutil.undefined_evars_of_term evm (EConstr.of_constr y) in
+ let evx = Evarutil.undefined_evars_of_term evm x in
+ let evy = Evarutil.undefined_evars_of_term evm y in
Intpart.union_set (Evar.Set.union evx evy) p)
cstrs
@@ -1076,7 +1076,7 @@ let error_unresolvable env comp evd =
| Some s -> Evar.Set.mem ev s
in
let fold ev evi (found, accu) =
- let ev_class = class_of_constr evd (EConstr.of_constr evi.evar_concl) in
+ let ev_class = class_of_constr evd evi.evar_concl in
if not (Option.is_empty ev_class) && is_part ev then
(* focus on one instance if only one was searched for *)
if not found then (true, Some ev)
@@ -1174,7 +1174,7 @@ let solve_inst env evd filter unique split fail =
let _ =
Hook.set Typeclasses.solve_all_instances_hook solve_inst
-let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique =
+let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique =
let nc, gl, subst, _ = Evarutil.push_rel_context_to_named_context env sigma gl in
let (gl,t,sigma) =
Goal.V82.mk_goal sigma nc gl Store.empty in
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index dc310c542d..3df9e3f820 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -70,11 +70,10 @@ let first_goal gls =
(* tactic -> tactic_list : Apply a tactic to the first goal in the list *)
let apply_tac_list tac glls =
- let (sigr,lg) = unpackage glls in
- match lg with
+ match glls.it with
| (g1::rest) ->
- let gl = apply_sig_tac sigr tac g1 in
- repackage sigr (gl@rest)
+ let pack = tac (re_sig g1 glls.sigma) in
+ re_sig (pack.it @ rest) pack.sigma
| _ -> user_err Pp.(str "apply_tac_list")
let one_step l gl =
@@ -90,7 +89,7 @@ let rec prolog l n gl =
let out_term env = function
| IsConstr (c, _) -> c
- | IsGlobRef gr -> EConstr.of_constr (fst (Universes.fresh_global_instance env gr))
+ | IsGlobRef gr -> EConstr.of_constr (fst (UnivGen.fresh_global_instance env gr))
let prolog_tac l n =
Proofview.V82.tactic begin fun gl ->
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 6bd4866c61..70f73df5c1 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -46,8 +46,8 @@ let optimize_non_type_induction_scheme kind dep sort _ ind =
mib.mind_nparams in
let sigma, sort = Evd.fresh_sort_in_family env sigma sort in
let sigma, t', c' = weaken_sort_scheme env sigma false sort npars c t in
- let sigma, nf = Evarutil.nf_evars_and_universes sigma in
- (nf c', Evd.evar_universe_context sigma), eff
+ let sigma = Evd.minimize_universes sigma in
+ (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma), eff
else
let sigma, pind = Evd.fresh_inductive_instance env sigma ind in
let sigma, c = build_induction_scheme env sigma pind dep sort in
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 477de6452e..eede133291 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -78,7 +78,7 @@ let build_dependent_inductive ind (mib,mip) =
Context.Rel.to_extended_list mkRel mip.mind_nrealdecls mib.mind_params_ctxt
@ Context.Rel.to_extended_list mkRel 0 realargs)
-let named_hd env t na = named_hd env Evd.empty (EConstr.of_constr t) na
+let named_hd env t na = named_hd env (Evd.from_env env) (EConstr.of_constr t) na
let name_assumption env = function
| LocalAssum (na,t) -> LocalAssum (named_hd env t na, t)
| LocalDef (na,c,t) -> LocalDef (named_hd env c na, c, t)
@@ -102,14 +102,14 @@ let get_coq_eq ctx =
let eq = Globnames.destIndRef Coqlib.glob_eq in
(* Do not force the lazy if they are not defined *)
let eq, ctx = with_context_set ctx
- (Universes.fresh_inductive_instance (Global.env ()) eq) in
+ (UnivGen.fresh_inductive_instance (Global.env ()) eq) in
mkIndU eq, mkConstructUi (eq,1), ctx
with Not_found ->
user_err Pp.(str "eq not found.")
let univ_of_eq env eq =
let eq = EConstr.of_constr eq in
- match Constr.kind (EConstr.Unsafe.to_constr (Retyping.get_type_of env Evd.empty eq)) with
+ match Constr.kind (EConstr.Unsafe.to_constr (Retyping.get_type_of env (Evd.from_env env) eq)) with
| Prod (_,t,_) -> (match Constr.kind t with Sort (Type u) -> u | _ -> assert false)
| _ -> assert false
@@ -192,7 +192,7 @@ let get_non_sym_eq_data env (ind,u) =
(**********************************************************************)
let build_sym_scheme env ind =
- let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
+ let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
get_sym_eq_data env indu in
let cstr n =
@@ -241,11 +241,11 @@ let sym_scheme_kind =
let const_of_scheme kind env ind ctx =
let sym_scheme, eff = (find_scheme kind ind) in
let sym, ctx = with_context_set ctx
- (Universes.fresh_constant_instance (Global.env()) sym_scheme) in
+ (UnivGen.fresh_constant_instance (Global.env()) sym_scheme) in
mkConstU sym, ctx, eff
let build_sym_involutive_scheme env ind =
- let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
+ let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
get_sym_eq_data env indu in
let eq,eqrefl,ctx = get_coq_eq ctx in
@@ -353,7 +353,7 @@ let sym_involutive_scheme_kind =
(**********************************************************************)
let build_l2r_rew_scheme dep env ind kind =
- let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
+ let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
get_sym_eq_data env indu in
let sym, ctx, eff = const_of_scheme sym_scheme_kind env ind ctx in
@@ -392,7 +392,7 @@ let build_l2r_rew_scheme dep env ind kind =
rel_vect (nrealargs+4) nrealargs;
rel_vect 1 nrealargs;
[|mkRel 1|]]) in
- let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in
+ let s, ctx' = UnivGen.fresh_sort_in_family (Global.env ()) kind in
let ctx = Univ.ContextSet.union ctx ctx' in
let s = mkSort s in
let ci = make_case_info (Global.env()) ind RegularStyle in
@@ -469,7 +469,7 @@ let build_l2r_rew_scheme dep env ind kind =
(**********************************************************************)
let build_l2r_forward_rew_scheme dep env ind kind =
- let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
+ let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
get_sym_eq_data env indu in
let cstr n p =
@@ -495,7 +495,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in
let realsign_ind_P n aP =
name_context env ((LocalAssum (Name varH,aP))::realsign_P n) in
- let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in
+ let s, ctx' = UnivGen.fresh_sort_in_family (Global.env ()) kind in
let ctx = Univ.ContextSet.union ctx ctx' in
let s = mkSort s in
let ci = make_case_info (Global.env()) ind RegularStyle in
@@ -561,7 +561,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
(**********************************************************************)
let build_r2l_forward_rew_scheme dep env ind kind =
- let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
+ let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
let ((mib,mip as specif),constrargs,realsign,paramsctxt,nrealargs) =
get_non_sym_eq_data env indu in
let cstr n =
@@ -573,7 +573,7 @@ let build_r2l_forward_rew_scheme dep env ind kind =
let applied_ind = build_dependent_inductive indu specif in
let realsign_ind =
name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in
- let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in
+ let s, ctx' = UnivGen.fresh_sort_in_family (Global.env ()) kind in
let ctx = Univ.ContextSet.union ctx ctx' in
let s = mkSort s in
let ci = make_case_info (Global.env()) ind RegularStyle in
@@ -620,7 +620,9 @@ let build_r2l_forward_rew_scheme dep env ind kind =
(**********************************************************************)
let fix_r2l_forward_rew_scheme (c, ctx') =
- let t = Retyping.get_type_of (Global.env()) Evd.empty (EConstr.of_constr c) in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let t = Retyping.get_type_of env sigma (EConstr.of_constr c) in
let t = EConstr.Unsafe.to_constr t in
let ctx,_ = decompose_prod_assum t in
match ctx with
@@ -630,7 +632,7 @@ let fix_r2l_forward_rew_scheme (c, ctx') =
(mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 1) p)
(mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 2) hp)
(mkLambda_or_LetIn (RelDecl.map_constr (lift 2) ind)
- (EConstr.Unsafe.to_constr (Reductionops.whd_beta Evd.empty
+ (EConstr.Unsafe.to_constr (Reductionops.whd_beta sigma
(EConstr.of_constr (applist (c,
Context.Rel.to_extended_list mkRel 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))))
in c', ctx'
@@ -755,7 +757,7 @@ let rew_r2l_scheme_kind =
let build_congr env (eq,refl,ctx) ind =
let (ind,u as indu), ctx = with_context_set ctx
- (Universes.fresh_inductive_instance env ind) in
+ (UnivGen.fresh_inductive_instance env ind) in
let (mib,mip) = lookup_mind_specif env ind in
if not (Int.equal (Array.length mib.mind_packets) 1) || not (Int.equal (Array.length mip.mind_nf_lc) 1) then
error "Not an inductive type with a single constructor.";
@@ -778,7 +780,7 @@ let build_congr env (eq,refl,ctx) ind =
let varH = fresh env (Id.of_string "H") in
let varf = fresh env (Id.of_string "f") in
let ci = make_case_info (Global.env()) ind RegularStyle in
- let uni, ctx = Universes.extend_context (Universes.new_global_univ ()) ctx in
+ let uni, ctx = UnivGen.extend_context (UnivGen.new_global_univ ()) ctx in
let ctx = (fst ctx, Univ.enforce_leq uni (univ_of_eq env eq) (snd ctx)) in
let c =
my_it_mkLambda_or_LetIn paramsctxt
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 98f627f211..8904cd170b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1108,8 +1108,6 @@ let make_tuple env sigma (rterm,rty) lind =
let p = mkLambda (na, a, rty) in
let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in
let sigma, sig_term = Evd.fresh_global env sigma sigdata.typ in
- let exist_term = EConstr.of_constr exist_term in
- let sig_term = EConstr.of_constr sig_term in
sigma,
(applist(exist_term,[a;p;(mkRel lind);rterm]),
applist(sig_term,[a;p]))
@@ -1178,35 +1176,35 @@ let minimal_free_rels_rec env sigma =
let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
let sigdata = find_sigma_data env sort_of_ty in
- let evdref = ref (Evd.clear_metas sigma) in
- let rec sigrec_clausal_form siglen p_i =
+ let rec sigrec_clausal_form sigma siglen p_i =
if Int.equal siglen 0 then
(* is the default value typable with the expected type *)
let dflt_typ = unsafe_type_of env sigma dflt in
try
- let () = evdref := Evarconv.the_conv_x_leq env dflt_typ p_i !evdref in
- let () =
- evdref := Evarconv.solve_unif_constraints_with_heuristics env !evdref in
- dflt
+ let sigma = Evarconv.the_conv_x_leq env dflt_typ p_i sigma in
+ let sigma =
+ Evarconv.solve_unif_constraints_with_heuristics env sigma in
+ sigma, dflt
with Evarconv.UnableToUnify _ ->
user_err Pp.(str "Cannot solve a unification problem.")
else
- let (a,p_i_minus_1) = match whd_beta_stack !evdref p_i with
+ let (a,p_i_minus_1) = match whd_beta_stack sigma p_i with
| (_sigS,[a;p]) -> (a, p)
| _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type.") in
- let ev = Evarutil.e_new_evar env evdref a in
+ let sigma, ev = Evarutil.new_evar env sigma a in
let rty = beta_applist sigma (p_i_minus_1,[ev]) in
- let tuple_tail = sigrec_clausal_form (siglen-1) rty in
- let evopt = match EConstr.kind !evdref ev with Evar _ -> None | _ -> Some ev in
+ let sigma, tuple_tail = sigrec_clausal_form sigma (siglen-1) rty in
+ let evopt = match EConstr.kind sigma ev with Evar _ -> None | _ -> Some ev in
match evopt with
| Some w ->
- let w_type = unsafe_type_of env !evdref w in
- if Evarconv.e_cumul env evdref w_type a then
- let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in
- let exist_term = EConstr.of_constr exist_term in
- applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
- else
+ let w_type = unsafe_type_of env sigma w in
+ begin match Evarconv.cumul env sigma w_type a with
+ | Some sigma ->
+ let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in
+ sigma, applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
+ | None ->
user_err Pp.(str "Cannot solve a unification problem.")
+ end
| None ->
(* This at least happens if what has been detected as a
dependency is not one; use an evasive error message;
@@ -1216,8 +1214,9 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
unsolved evars would mean not binding rel *)
user_err Pp.(str "Cannot solve a unification problem.")
in
- let scf = sigrec_clausal_form siglen ty in
- !evdref, Evarutil.nf_evar !evdref scf
+ let sigma = Evd.clear_metas sigma in
+ let sigma, scf = sigrec_clausal_form sigma siglen ty in
+ sigma, Evarutil.nf_evar sigma scf
(* The problem is to build a destructor (a generalization of the
predecessor) which, when applied to a term made of constructors
@@ -1372,7 +1371,6 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
let sigma, (injbody,resty) = build_injector e_env !evdref t1' (mkVar e) cpath in
let injfun = mkNamedLambda e t injbody in
let sigma,congr = Evd.fresh_global env sigma eq.congr in
- let congr = EConstr.of_constr congr in
let pf = applist(congr,[t;resty;injfun;t1;t2]) in
let sigma, pf_typ = Typing.type_of env sigma pf in
let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
@@ -1761,8 +1759,17 @@ type subst_tactic_flags = {
let default_subst_tactic_flags =
{ only_leibniz = false; rewrite_dependent_proof = true }
+let warn_deprecated_simple_subst =
+ CWarnings.create ~name:"deprecated-simple-subst" ~category:"deprecated"
+ (fun () -> strbrk"\"simple subst\" is deprecated")
+
let subst_all ?(flags=default_subst_tactic_flags) () =
+ let () =
+ if flags.only_leibniz || not flags.rewrite_dependent_proof then
+ warn_deprecated_simple_subst ()
+ in
+
if !regular_subst_tactic then
(* First step: find hypotheses to treat in linear time *)
@@ -1774,7 +1781,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
try
let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in
let u = EInstance.kind sigma u in
- let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
+ let eq = UnivGen.constr_of_global_univ (lbeq.eq,u) in
if flags.only_leibniz then restrict_to_eq_and_identity eq;
match EConstr.kind sigma x, EConstr.kind sigma y with
| Var z, _ when not (is_evaluable env (EvalVarRef z)) ->
@@ -1825,7 +1832,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
try
let lbeq,u,(_,x,y) = find_eq_data_decompose c in
let u = EInstance.kind sigma u in
- let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
+ let eq = UnivGen.constr_of_global_univ (lbeq.eq,u) in
if flags.only_leibniz then restrict_to_eq_and_identity eq;
(* J.F.: added to prevent failure on goal containing x=x as an hyp *)
if EConstr.eq_constr sigma x y then failwith "caught";
diff --git a/tactics/equality.mli b/tactics/equality.mli
index c0be917a08..ccf454c3e1 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -80,20 +80,20 @@ val discrConcl : unit Proofview.tactic
val discrHyp : Id.t -> unit Proofview.tactic
val discrEverywhere : evars_flag -> unit Proofview.tactic
val discr_tac : evars_flag ->
- constr with_bindings destruction_arg option -> unit Proofview.tactic
+ constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic
(* Below, if flag is [None], it takes the value from the dynamic value of the option *)
val inj : inj_flags option -> intro_patterns option -> evars_flag ->
clear_flag -> constr with_bindings -> unit Proofview.tactic
val injClause : inj_flags option -> intro_patterns option -> evars_flag ->
- constr with_bindings destruction_arg option -> unit Proofview.tactic
+ constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic
val injHyp : inj_flags option -> clear_flag -> Id.t -> unit Proofview.tactic
val injConcl : inj_flags option -> unit Proofview.tactic
val simpleInjClause : inj_flags option -> evars_flag ->
- constr with_bindings destruction_arg option -> unit Proofview.tactic
+ constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic
-val dEq : keep_proofs:(bool option) -> evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic
-val dEqThen : keep_proofs:(bool option) -> evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings destruction_arg option -> unit Proofview.tactic
+val dEq : keep_proofs:(bool option) -> evars_flag -> constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic
+val dEqThen : keep_proofs:(bool option) -> evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic
val make_iterated_tuple :
env -> evar_map -> constr -> (constr * types) -> evar_map * (constr * constr * constr)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index a285d6b93f..786760122a 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -28,12 +28,13 @@ open Termops
open Inductiveops
open Typing
open Decl_kinds
+open Vernacexpr
+open Typeclasses
open Pattern
open Patternops
open Clenv
open Tacred
open Printer
-open Vernacexpr
module NamedDecl = Context.Named.Declaration
@@ -94,7 +95,6 @@ let secvars_of_hyps hyps =
else pred
let empty_hint_info =
- let open Vernacexpr in
{ hint_priority = None; hint_pattern = None }
(************************************************************************)
@@ -115,7 +115,7 @@ type 'a hints_path_atom_gen =
(* For forward hints, their names is the list of projections *)
| PathAny
-type hints_path_atom = global_reference hints_path_atom_gen
+type hints_path_atom = GlobRef.t hints_path_atom_gen
type 'a hints_path_gen =
| PathAtom of 'a hints_path_atom_gen
@@ -126,10 +126,10 @@ type 'a hints_path_gen =
| PathEpsilon
type pre_hints_path = Libnames.reference hints_path_gen
-type hints_path = global_reference hints_path_gen
+type hints_path = GlobRef.t hints_path_gen
type hint_term =
- | IsGlobRef of global_reference
+ | IsGlobRef of GlobRef.t
| IsConstr of constr * Univ.ContextSet.t
type 'a with_uid = {
@@ -153,7 +153,7 @@ type 'a with_metadata = {
type full_hint = hint with_metadata
-type hint_entry = global_reference option *
+type hint_entry = GlobRef.t option *
raw_hint hint_ast with_uid with_metadata
type import_level = [ `LAX | `WARN | `STRICT ]
@@ -308,7 +308,7 @@ let instantiate_hint env sigma p =
{ p with code = { p.code with obj = code } }
let hints_path_atom_eq h1 h2 = match h1, h2 with
-| PathHints l1, PathHints l2 -> List.equal eq_gr l1 l2
+| PathHints l1, PathHints l2 -> List.equal GlobRef.equal l1 l2
| PathAny, PathAny -> true
| _ -> false
@@ -365,7 +365,7 @@ let path_seq p p' =
let rec path_derivate hp hint =
let rec derivate_atoms hints hints' =
match hints, hints' with
- | gr :: grs, gr' :: grs' when eq_gr gr gr' -> derivate_atoms grs grs'
+ | gr :: grs, gr' :: grs' when GlobRef.equal gr gr' -> derivate_atoms grs grs'
| [], [] -> PathEpsilon
| [], hints -> PathEmpty
| grs, [] -> PathAtom (PathHints grs)
@@ -448,7 +448,7 @@ let subst_path_atom subst p =
| PathAny -> p
| PathHints grs ->
let gr' gr = fst (subst_global subst gr) in
- let grs' = List.smartmap gr' grs in
+ let grs' = List.Smart.map gr' grs in
if grs' == grs then p else PathHints grs'
let rec subst_hints_path subst hp =
@@ -474,28 +474,28 @@ module Hint_db :
sig
type t
val empty : ?name:hint_db_name -> transparent_state -> bool -> t
-val find : global_reference -> t -> search_entry
+val find : GlobRef.t -> t -> search_entry
val map_none : secvars:Id.Pred.t -> t -> full_hint list
-val map_all : secvars:Id.Pred.t -> global_reference -> t -> full_hint list
+val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list
val map_existential : evar_map -> secvars:Id.Pred.t ->
- (global_reference * constr array) -> constr -> t -> full_hint list
+ (GlobRef.t * constr array) -> constr -> t -> full_hint list
val map_eauto : evar_map -> secvars:Id.Pred.t ->
- (global_reference * constr array) -> constr -> t -> full_hint list
+ (GlobRef.t * constr array) -> constr -> t -> full_hint list
val map_auto : evar_map -> secvars:Id.Pred.t ->
- (global_reference * constr array) -> constr -> t -> full_hint list
+ (GlobRef.t * constr array) -> constr -> t -> full_hint list
val add_one : env -> evar_map -> hint_entry -> t -> t
val add_list : env -> evar_map -> hint_entry list -> t -> t
-val remove_one : global_reference -> t -> t
-val remove_list : global_reference list -> t -> t
-val iter : (global_reference option -> hint_mode array list -> full_hint list -> unit) -> t -> unit
+val remove_one : GlobRef.t -> t -> t
+val remove_list : GlobRef.t list -> t -> t
+val iter : (GlobRef.t option -> hint_mode array list -> full_hint list -> unit) -> t -> unit
val use_dn : t -> bool
val transparent_state : t -> transparent_state
val set_transparent_state : t -> transparent_state -> t
val add_cut : hints_path -> t -> t
-val add_mode : global_reference -> hint_mode array -> t -> t
+val add_mode : GlobRef.t -> hint_mode array -> t -> t
val cut : t -> hints_path
val unfolds : t -> Id.Set.t * Cset.t
-val fold : (global_reference option -> hint_mode array list -> full_hint list -> 'a -> 'a) ->
+val fold : (GlobRef.t option -> hint_mode array list -> full_hint list -> 'a -> 'a) ->
t -> 'a -> 'a
end =
@@ -510,7 +510,7 @@ struct
hintdb_map : search_entry Constr_map.t;
(* A list of unindexed entries starting with an unfoldable constant
or with no associated pattern. *)
- hintdb_nopat : (global_reference option * stored_data) list;
+ hintdb_nopat : (GlobRef.t option * stored_data) list;
hintdb_name : string option;
}
@@ -654,7 +654,7 @@ struct
let add_list env sigma l db = List.fold_left (fun db k -> add_one env sigma k db) db l
- let remove_sdl p sdl = List.smartfilter p sdl
+ let remove_sdl p sdl = List.Smart.filter p sdl
let remove_he st p se =
let sl1' = remove_sdl p se.sentry_nopat in
@@ -664,9 +664,9 @@ struct
let remove_list grs db =
let filter (_, h) =
- match h.name with PathHints [gr] -> not (List.mem_f eq_gr gr grs) | _ -> true in
+ match h.name with PathHints [gr] -> not (List.mem_f GlobRef.equal gr grs) | _ -> true in
let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in
- let hintnopat = List.smartfilter (fun (ge, sd) -> filter sd) db.hintdb_nopat in
+ let hintnopat = List.Smart.filter (fun (ge, sd) -> filter sd) db.hintdb_nopat in
{ db with hintdb_map = hintmap; hintdb_nopat = hintnopat }
let remove_one gr db = remove_list [gr] db
@@ -792,7 +792,7 @@ let make_exact_entry env sigma info poly ?(name=PathAny) (c, cty, ctx) =
match EConstr.kind sigma cty with
| Prod _ -> failwith "make_exact_entry"
| _ ->
- let pat = Patternops.pattern_of_constr env sigma (EConstr.to_constr sigma cty) in
+ let pat = Patternops.pattern_of_constr env sigma (EConstr.to_constr ~abort_on_undefined_evars:false sigma cty) in
let hd =
try head_pattern_bound pat
with BoundPattern -> failwith "make_exact_entry"
@@ -814,7 +814,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) info poly ?(name=PathAny) (c
let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
let ce = mk_clenv_from_env env sigma' None (c,cty) in
let c' = clenv_type (* ~reduce:false *) ce in
- let pat = Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma c') in
+ let pat = Patternops.pattern_of_constr env ce.evd (EConstr.to_constr ~abort_on_undefined_evars:false sigma c') in
let hd =
try head_pattern_bound pat
with BoundPattern -> failwith "make_apply_entry" in
@@ -876,7 +876,7 @@ let fresh_global_or_constr env sigma poly cr =
let isgr, (c, ctx) =
match cr with
| IsGlobRef gr ->
- let (c, ctx) = Universes.fresh_global_instance env gr in
+ let (c, ctx) = UnivGen.fresh_global_instance env gr in
true, (EConstr.of_constr c, ctx)
| IsConstr (c, ctx) -> false, (c, ctx)
in
@@ -1015,9 +1015,9 @@ type hint_action =
| CreateDB of bool * transparent_state
| AddTransparency of evaluable_global_reference list * bool
| AddHints of hint_entry list
- | RemoveHints of global_reference list
+ | RemoveHints of GlobRef.t list
| AddCut of hints_path
- | AddMode of global_reference * hint_mode array
+ | AddMode of GlobRef.t * hint_mode array
let add_cut dbname path =
let db = get_db dbname in
@@ -1065,8 +1065,8 @@ let subst_autohint (subst, obj) =
in if gr' == gr then gr else gr'
in
let subst_hint (k,data as hint) =
- let k' = Option.smartmap subst_key k in
- let pat' = Option.smartmap (subst_pattern subst) data.pat in
+ let k' = Option.Smart.map subst_key k in
+ let pat' = Option.Smart.map (subst_pattern subst) data.pat in
let subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in
let code' = match data.code.obj with
| Res_pf (c,t,ctx) ->
@@ -1104,13 +1104,13 @@ let subst_autohint (subst, obj) =
let action = match obj.hint_action with
| CreateDB _ -> obj.hint_action
| AddTransparency (grs, b) ->
- let grs' = List.smartmap (subst_evaluable_reference subst) grs in
+ let grs' = List.Smart.map (subst_evaluable_reference subst) grs in
if grs == grs' then obj.hint_action else AddTransparency (grs', b)
| AddHints hintlist ->
- let hintlist' = List.smartmap subst_hint hintlist in
+ let hintlist' = List.Smart.map subst_hint hintlist in
if hintlist' == hintlist then obj.hint_action else AddHints hintlist'
| RemoveHints grs ->
- let grs' = List.smartmap (subst_global_reference subst) grs in
+ let grs' = List.Smart.map (subst_global_reference subst) grs in
if grs == grs' then obj.hint_action else RemoveHints grs'
| AddCut path ->
let path' = subst_hints_path subst path in
@@ -1226,7 +1226,7 @@ type hints_entry =
| HintsCutEntry of hints_path
| HintsUnfoldEntry of evaluable_global_reference list
| HintsTransparencyEntry of evaluable_global_reference list * bool
- | HintsModeEntry of global_reference * hint_mode list
+ | HintsModeEntry of GlobRef.t * hint_mode list
| HintsExternEntry of hint_info * Genarg.glob_generic_argument
let default_prepare_hint_ident = Id.of_string "H"
@@ -1263,7 +1263,9 @@ let prepare_hint check (poly,local) env init (sigma,c) =
subst := (evar,mkVar id)::!subst;
mkNamedLambda id t (iter (replace_term sigma evar (mkVar id) c)) in
let c' = iter c in
- if check then Pretyping.check_evars (Global.env()) Evd.empty sigma c';
+ let env = Global.env () in
+ let empty_sigma = Evd.from_env env in
+ if check then Pretyping.check_evars env empty_sigma sigma c';
let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
if poly then IsConstr (c', diff)
else if local then IsConstr (c', diff)
@@ -1276,7 +1278,9 @@ let interp_hints poly =
let sigma = Evd.from_env env in
let f poly c =
let evd,c = Constrintern.interp_open_constr env sigma c in
- prepare_hint true (poly,false) (Global.env()) Evd.empty (evd,c) in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ prepare_hint true (poly,false) env sigma (evd,c) in
let fref r =
let gr = global_with_alias r in
Dumpglob.add_glob ?loc:r.CAst.loc gr;
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 1811150c2a..c7de10a2a5 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -12,7 +12,6 @@ open Util
open Names
open EConstr
open Environ
-open Globnames
open Decl_kinds
open Evd
open Misctypes
@@ -25,13 +24,13 @@ open Vernacexpr
exception Bound
-val decompose_app_bound : evar_map -> constr -> global_reference * constr array
+val decompose_app_bound : evar_map -> constr -> GlobRef.t * constr array
type debug = Debug | Info | Off
val secvars_of_hyps : ('c, 't) Context.Named.pt -> Id.Pred.t
-val empty_hint_info : 'a hint_info_gen
+val empty_hint_info : 'a Typeclasses.hint_info_gen
(** Pre-created hint databases *)
@@ -51,7 +50,7 @@ type 'a hints_path_atom_gen =
(* For forward hints, their names is the list of projections *)
| PathAny
-type hints_path_atom = global_reference hints_path_atom_gen
+type hints_path_atom = GlobRef.t hints_path_atom_gen
type hint_db_name = string
type 'a with_metadata = private {
@@ -81,7 +80,7 @@ type 'a hints_path_gen =
| PathEpsilon
type pre_hints_path = Libnames.reference hints_path_gen
-type hints_path = global_reference hints_path_gen
+type hints_path = GlobRef.t hints_path_gen
val normalize_path : hints_path -> hints_path
val path_matches : hints_path -> hints_path_atom list -> bool
@@ -91,15 +90,15 @@ val pp_hints_path_atom : ('a -> Pp.t) -> 'a hints_path_atom_gen -> Pp.t
val pp_hints_path : hints_path -> Pp.t
val pp_hint_mode : hint_mode -> Pp.t
val glob_hints_path_atom :
- Libnames.reference hints_path_atom_gen -> Globnames.global_reference hints_path_atom_gen
+ Libnames.reference hints_path_atom_gen -> GlobRef.t hints_path_atom_gen
val glob_hints_path :
- Libnames.reference hints_path_gen -> Globnames.global_reference hints_path_gen
+ Libnames.reference hints_path_gen -> GlobRef.t hints_path_gen
module Hint_db :
sig
type t
val empty : ?name:hint_db_name -> transparent_state -> bool -> t
- val find : global_reference -> t -> search_entry
+ val find : GlobRef.t -> t -> search_entry
(** All hints which have no pattern.
* [secvars] represent the set of section variables that
@@ -107,27 +106,27 @@ module Hint_db :
val map_none : secvars:Id.Pred.t -> t -> full_hint list
(** All hints associated to the reference *)
- val map_all : secvars:Id.Pred.t -> global_reference -> t -> full_hint list
+ val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list
(** All hints associated to the reference, respecting modes if evars appear in the
arguments, _not_ using the discrimination net. *)
val map_existential : evar_map -> secvars:Id.Pred.t ->
- (global_reference * constr array) -> constr -> t -> full_hint list
+ (GlobRef.t * constr array) -> constr -> t -> full_hint list
(** All hints associated to the reference, respecting modes if evars appear in the
arguments and using the discrimination net. *)
- val map_eauto : evar_map -> secvars:Id.Pred.t -> (global_reference * constr array) -> constr -> t -> full_hint list
+ val map_eauto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> full_hint list
(** All hints associated to the reference, respecting modes if evars appear in the
arguments. *)
val map_auto : evar_map -> secvars:Id.Pred.t ->
- (global_reference * constr array) -> constr -> t -> full_hint list
+ (GlobRef.t * constr array) -> constr -> t -> full_hint list
val add_one : env -> evar_map -> hint_entry -> t -> t
val add_list : env -> evar_map -> hint_entry list -> t -> t
- val remove_one : global_reference -> t -> t
- val remove_list : global_reference list -> t -> t
- val iter : (global_reference option ->
+ val remove_one : GlobRef.t -> t -> t
+ val remove_list : GlobRef.t list -> t -> t
+ val iter : (GlobRef.t option ->
hint_mode array list -> full_hint list -> unit) -> t -> unit
val use_dn : t -> bool
@@ -144,10 +143,10 @@ type hint_db = Hint_db.t
type hnf = bool
-type hint_info = (patvar list * constr_pattern) hint_info_gen
+type hint_info = (patvar list * constr_pattern) Typeclasses.hint_info_gen
type hint_term =
- | IsGlobRef of global_reference
+ | IsGlobRef of GlobRef.t
| IsConstr of constr * Univ.ContextSet.t
type hints_entry =
@@ -157,7 +156,7 @@ type hints_entry =
| HintsCutEntry of hints_path
| HintsUnfoldEntry of evaluable_global_reference list
| HintsTransparencyEntry of evaluable_global_reference list * bool
- | HintsModeEntry of global_reference * hint_mode list
+ | HintsModeEntry of GlobRef.t * hint_mode list
| HintsExternEntry of hint_info * Genarg.glob_generic_argument
val searchtable_map : hint_db_name -> hint_db
@@ -171,7 +170,7 @@ val searchtable_add : (hint_db_name * hint_db) -> unit
val create_hint_db : bool -> hint_db_name -> transparent_state -> bool -> unit
-val remove_hints : bool -> hint_db_name list -> global_reference list -> unit
+val remove_hints : bool -> hint_db_name list -> GlobRef.t list -> unit
val current_db_names : unit -> String.Set.t
@@ -264,7 +263,7 @@ val rewrite_db : hint_db_name
val pr_searchtable : env -> evar_map -> Pp.t
val pr_applicable_hint : unit -> Pp.t
-val pr_hint_ref : env -> evar_map -> global_reference -> Pp.t
+val pr_hint_ref : env -> evar_map -> GlobRef.t -> Pp.t
val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t
val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t
val pr_hint_db : Hint_db.t -> Pp.t
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index b012a7ecd1..b8f1ed720b 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -294,13 +294,13 @@ let match_with_equation env sigma t =
let (hdapp,args) = destApp sigma t in
match EConstr.kind sigma hdapp with
| Ind (ind,u) ->
- if eq_gr (IndRef ind) glob_eq then
+ if GlobRef.equal (IndRef ind) glob_eq then
Some (build_coq_eq_data()),hdapp,
PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
- else if eq_gr (IndRef ind) glob_identity then
+ else if GlobRef.equal (IndRef ind) glob_identity then
Some (build_coq_identity_data()),hdapp,
PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
- else if eq_gr (IndRef ind) glob_jmeq then
+ else if GlobRef.equal (IndRef ind) glob_jmeq then
Some (build_coq_jmeq_data()),hdapp,
HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
else
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 0697d0f19c..f04cda1232 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -144,7 +144,7 @@ val is_matching_sigma : Environ.env -> evar_map -> constr -> bool
(** Match a decidable equality judgement (e.g [{t=u:>T}+{~t=u}]), returns
[t,u,T] and a boolean telling if equality is on the left side *)
-val match_eqdec : Environ.env -> evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr
+val match_eqdec : Environ.env -> evar_map -> constr -> bool * GlobRef.t * constr * constr * constr
(** Match a negation *)
val is_matching_not : Environ.env -> evar_map -> constr -> bool
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 62ead57f38..21520f5d2b 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -53,7 +53,7 @@ let subst_one_scheme subst (ind,const) =
(subst_ind subst ind,subst_constant subst const)
let subst_scheme (subst,(kind,l)) =
- (kind,Array.map (subst_one_scheme subst) l)
+ (kind,Array.Smart.map (subst_one_scheme subst) l)
let discharge_scheme (_,(kind,l)) =
Some (kind,Array.map (fun (ind,const) ->
@@ -123,7 +123,7 @@ let define internal id c p univs =
let fd = declare_constant ~internal in
let id = compute_name internal id in
let ctx = UState.minimize univs in
- let c = Universes.subst_opt_univs_constr (UState.subst ctx) c in
+ let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in
let univs =
if p then Polymorphic_const_entry (UState.context ctx)
else Monomorphic_const_entry (UState.context_set ctx)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 067fc8941a..b346ed2230 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -64,6 +64,11 @@ let var_occurs_in_pf gl id =
type inversion_status = Dep of constr option | NoDep
+type inversion_kind =
+ | SimpleInversion
+ | FullInversion
+ | FullInversionClear
+
let compute_eqn env sigma n i ai =
(mkRel (n-i),get_type_of env sigma (mkRel (n-i)))
@@ -119,12 +124,10 @@ let make_inv_predicate env evd indf realargs id status concl =
in
let eq_term = eqdata.Coqlib.eq in
let eq = Evarutil.evd_comb1 (Evd.fresh_global env) evd eq_term in
- let eq = EConstr.of_constr eq in
let eqn = applist (eq,[eqnty;lhs;rhs]) in
let eqns = (Anonymous, lift n eqn) :: eqns in
let refl_term = eqdata.Coqlib.refl in
let refl_term = Evarutil.evd_comb1 (Evd.fresh_global env) evd refl_term in
- let refl_term = EConstr.of_constr refl_term in
let refl = mkApp (refl_term, [|eqnty; rhs|]) in
let _ = Evarutil.evd_comb1 (Typing.type_of env) evd refl in
let args = refl :: args in
@@ -289,7 +292,7 @@ let error_too_many_names pats =
str "Unexpected " ++
str (String.plural (List.length pats) "introduction pattern") ++
str ": " ++ pr_enum (Miscprint.pr_intro_pattern
- (fun c -> Printer.pr_constr_env env sigma (EConstr.Unsafe.to_constr (snd (c env Evd.empty))))) pats ++
+ (fun c -> Printer.pr_constr_env env sigma (EConstr.Unsafe.to_constr (snd (c env (Evd.from_env env)))))) pats ++
str ".")
let get_names (allow_conj,issimple) ({CAst.loc;v=pat} as x) = match pat with
@@ -493,9 +496,10 @@ let wrap_inv_error id = function (e, info) -> match e with
| Indrec.RecursionSchemeError
(Indrec.NotAllowedCaseAnalysis (_,(Type _ | Prop Pos as k),i)) ->
Proofview.tclENV >>= fun env ->
+ Proofview.tclEVARMAP >>= fun sigma ->
tclZEROMSG (
(strbrk "Inversion would require case analysis on sort " ++
- pr_sort Evd.empty k ++
+ pr_sort sigma k ++
strbrk " which is not allowed for inductive definition " ++
pr_inductive env (fst i) ++ str "."))
| e -> Proofview.tclZERO ~info e
diff --git a/tactics/inv.mli b/tactics/inv.mli
index c63d57af54..9d4ffdd7b7 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -15,6 +15,11 @@ open Tactypes
type inversion_status = Dep of constr option | NoDep
+type inversion_kind =
+ | SimpleInversion
+ | FullInversion
+ | FullInversionClear
+
val inv_clause :
inversion_kind -> or_and_intro_pattern option -> Id.t list ->
quantified_hypothesis -> unit Proofview.tactic
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 958a205a15..6c7db26c77 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -263,7 +263,7 @@ let pf_with_evars glsev k gls =
tclTHEN (Refiner.tclEVARS evd) (k a) gls
let pf_constr_of_global gr k =
- pf_with_evars (fun gls -> on_snd EConstr.of_constr (pf_apply Evd.fresh_global gls gr)) k
+ pf_with_evars (fun gls -> pf_apply Evd.fresh_global gls gr) k
(** Tacticals of Ltac defined directly in term of Proofview *)
module New = struct
@@ -369,9 +369,36 @@ module New = struct
tclTHENSFIRSTn t1 l (tclUNIT())
let tclTHENFIRST t1 t2 =
tclTHENFIRSTn t1 [|t2|]
+
+ let tclBINDFIRST t1 t2 =
+ t1 >>= fun ans ->
+ Proofview.Unsafe.tclGETGOALS >>= fun gls ->
+ match gls with
+ | [] -> tclFAIL 0 (str "Expect at least one goal.")
+ | hd::tl ->
+ Proofview.Unsafe.tclSETGOALS [hd] <*> t2 ans >>= fun ans ->
+ Proofview.Unsafe.tclNEWGOALS tl <*>
+ Proofview.tclUNIT ans
+
let tclTHENLASTn t1 l =
tclTHENS3PARTS t1 [||] (tclUNIT()) l
let tclTHENLAST t1 t2 = tclTHENLASTn t1 [|t2|]
+
+ let option_of_failure f x = try Some (f x) with Failure _ -> None
+
+ let tclBINDLAST t1 t2 =
+ t1 >>= fun ans ->
+ Proofview.Unsafe.tclGETGOALS >>= fun gls ->
+ match option_of_failure List.sep_last gls with
+ | None -> tclFAIL 0 (str "Expect at least one goal.")
+ | Some (last,firstn) ->
+ Proofview.Unsafe.tclSETGOALS [last] <*> t2 ans >>= fun ans ->
+ Proofview.Unsafe.tclGETGOALS >>= fun newgls ->
+ tclEVARMAP >>= fun sigma ->
+ let firstn = Proofview.Unsafe.undefined sigma firstn in
+ Proofview.Unsafe.tclSETGOALS (firstn@newgls) <*>
+ Proofview.tclUNIT ans
+
let tclTHENS t l =
tclINDEPENDENT begin
t <*>Proofview.tclORELSE (* converts the [SizeMismatch] error into an ltac error *)
@@ -465,11 +492,13 @@ module New = struct
Proofview.tclINDEPENDENT (Proofview.tclPROGRESS t)
(* Select a subset of the goals *)
- let tclSELECT = function
- | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i
- | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l
- | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id
- | Vernacexpr.SelectAll -> fun tac -> tac
+ let tclSELECT = let open Goal_select in function
+ | SelectNth i -> Proofview.tclFOCUS i i
+ | SelectList l -> Proofview.tclFOCUSLIST l
+ | SelectId id -> Proofview.tclFOCUSID id
+ | SelectAll -> anomaly ~label:"tclSELECT" Pp.(str "SelectAll not allowed here")
+ | SelectAlreadyFocused ->
+ anomaly ~label:"tclSELECT" Pp.(str "SelectAlreadyFocused not allowed here")
(* Check that holes in arguments have been resolved *)
@@ -479,7 +508,7 @@ module New = struct
let evi = Evd.find sigma evk in
match Evd.evar_body evi with
| Evd.Evar_empty -> Some (evk,evi)
- | Evd.Evar_defined c -> match Constr.kind c with
+ | Evd.Evar_defined c -> match Constr.kind (EConstr.Unsafe.to_constr c) with
| Term.Evar (evk,l) -> is_undefined_up_to_restriction sigma evk
| _ ->
(* We make the assumption that there is no way to refine an
@@ -682,7 +711,7 @@ module New = struct
let gl_make_elim ind = begin fun gl ->
let gr = Indrec.lookup_eliminator (fst ind) (elimination_sort_of_goal gl) in
let (sigma, c) = pf_apply Evd.fresh_global gl gr in
- (sigma, EConstr.of_constr c)
+ (sigma, c)
end
let gl_make_case_dep (ind, u) = begin fun gl ->
@@ -742,7 +771,6 @@ module New = struct
Proofview.tclEVARMAP >>= fun sigma ->
Proofview.tclENV >>= fun env ->
let (sigma, c) = Evd.fresh_global env sigma ref in
- let c = EConstr.of_constr c in
Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT c
end
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index f0ebac780e..cbaf691f1f 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -135,7 +135,7 @@ val elimination_sort_of_hyp : Id.t -> goal sigma -> Sorts.family
val elimination_sort_of_clause : Id.t option -> goal sigma -> Sorts.family
val pf_with_evars : (goal sigma -> Evd.evar_map * 'a) -> ('a -> tactic) -> tactic
-val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> tactic
+val pf_constr_of_global : GlobRef.t -> (constr -> tactic) -> tactic
(** Tacticals defined directly in term of Proofview *)
@@ -196,8 +196,10 @@ module New : sig
(** [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls]
and [tac2] to the first resulting subgoal *)
val tclTHENFIRST : unit tactic -> unit tactic -> unit tactic
+ val tclBINDFIRST : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
val tclTHENLASTn : unit tactic -> unit tactic array -> unit tactic
val tclTHENLAST : unit tactic -> unit tactic -> unit tactic
+ val tclBINDLAST : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
(* [tclTHENS t l = t <*> tclDISPATCH l] *)
val tclTHENS : unit tactic -> unit tactic list -> unit tactic
(* [tclTHENLIST [t1;…;tn]] is [t1<*>…<*>tn] *)
@@ -221,7 +223,7 @@ module New : sig
val tclCOMPLETE : 'a tactic -> 'a tactic
val tclSOLVE : unit tactic list -> unit tactic
val tclPROGRESS : unit tactic -> unit tactic
- val tclSELECT : Vernacexpr.goal_selector -> 'a tactic -> 'a tactic
+ val tclSELECT : Goal_select.t -> 'a tactic -> 'a tactic
val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic
val tclDELAYEDWITHHOLES : bool -> 'a delayed_open -> ('a -> unit tactic) -> unit tactic
@@ -266,5 +268,5 @@ module New : sig
val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic
val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic
- val pf_constr_of_global : Globnames.global_reference -> constr Proofview.tactic
+ val pf_constr_of_global : GlobRef.t -> constr Proofview.tactic
end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index df3cca1447..a42e4b44b5 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -198,32 +198,40 @@ end
let convert x y = convert_gen Reduction.CONV x y
let convert_leq x y = convert_gen Reduction.CUMUL x y
-let clear_dependency_msg env sigma id = function
+let clear_in_global_msg = function
+ | None -> mt ()
+ | Some ref -> str " implicitly in " ++ Printer.pr_global ref
+
+let clear_dependency_msg env sigma id err inglobal =
+ let pp = clear_in_global_msg inglobal in
+ match err with
| Evarutil.OccurHypInSimpleClause None ->
- Id.print id ++ str " is used in conclusion."
+ Id.print id ++ str " is used" ++ pp ++ str " in conclusion."
| Evarutil.OccurHypInSimpleClause (Some id') ->
- Id.print id ++ strbrk " is used in hypothesis " ++ Id.print id' ++ str"."
+ Id.print id ++ strbrk " is used" ++ pp ++ str " in hypothesis " ++ Id.print id' ++ str"."
| Evarutil.EvarTypingBreak ev ->
str "Cannot remove " ++ Id.print id ++
strbrk " without breaking the typing of " ++
Printer.pr_existential env sigma ev ++ str"."
-let error_clear_dependency env sigma id err =
- user_err (clear_dependency_msg env sigma id err)
+let error_clear_dependency env sigma id err inglobal =
+ user_err (clear_dependency_msg env sigma id err inglobal)
-let replacing_dependency_msg env sigma id = function
+let replacing_dependency_msg env sigma id err inglobal =
+ let pp = clear_in_global_msg inglobal in
+ match err with
| Evarutil.OccurHypInSimpleClause None ->
- str "Cannot change " ++ Id.print id ++ str ", it is used in conclusion."
+ str "Cannot change " ++ Id.print id ++ str ", it is used" ++ pp ++ str " in conclusion."
| Evarutil.OccurHypInSimpleClause (Some id') ->
str "Cannot change " ++ Id.print id ++
- strbrk ", it is used in hypothesis " ++ Id.print id' ++ str"."
+ strbrk ", it is used" ++ pp ++ str " in hypothesis " ++ Id.print id' ++ str"."
| Evarutil.EvarTypingBreak ev ->
str "Cannot change " ++ Id.print id ++
strbrk " without breaking the typing of " ++
Printer.pr_existential env sigma ev ++ str"."
-let error_replacing_dependency env sigma id err =
- user_err (replacing_dependency_msg env sigma id err)
+let error_replacing_dependency env sigma id err inglobal =
+ user_err (replacing_dependency_msg env sigma id err inglobal)
(* This tactic enables the user to remove hypotheses from the signature.
* Some care is taken to prevent him from removing variables that are
@@ -239,13 +247,12 @@ let clear_gen fail = function
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let concl = Proofview.Goal.concl gl in
- let evdref = ref sigma in
- let (hyps, concl) =
- try clear_hyps_in_evi env evdref (named_context_val env) concl ids
- with Evarutil.ClearDependencyError (id,err) -> fail env sigma id err
+ let (sigma, hyps, concl) =
+ try clear_hyps_in_evi env sigma (named_context_val env) concl ids
+ with Evarutil.ClearDependencyError (id,err,inglobal) -> fail env sigma id err inglobal
in
let env = reset_with_named_context hyps env in
- Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref)
+ Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(Refine.refine ~typecheck:false begin fun sigma ->
Evarutil.new_evar env sigma ~principal:true concl
end)
@@ -423,11 +430,10 @@ let get_previous_hyp_position env sigma id =
let clear_hyps2 env sigma ids sign t cl =
try
- let evdref = ref (Evd.clear_metas sigma) in
- let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in
- (hyps, t, cl, !evdref)
- with Evarutil.ClearDependencyError (id,err) ->
- error_replacing_dependency env sigma id err
+ let sigma = Evd.clear_metas sigma in
+ Evarutil.clear_hyps2_in_evi env sigma sign t cl ids
+ with Evarutil.ClearDependencyError (id,err,inglobal) ->
+ error_replacing_dependency env sigma id err inglobal
let internal_cut_gen ?(check=true) dir replace id t =
Proofview.Goal.enter begin fun gl ->
@@ -439,7 +445,7 @@ let internal_cut_gen ?(check=true) dir replace id t =
let sign',t,concl,sigma =
if replace then
let nexthyp = get_next_hyp_position env sigma id (named_context_of_val sign) in
- let sign',t,concl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in
+ let sigma,sign',t,concl = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in
let sign' = insert_decl_in_named_context sigma (LocalAssum (id,t)) nexthyp sign' in
sign',t,concl,sigma
else
@@ -557,15 +563,7 @@ let mutual_fix f n rest j = Proofview.Goal.enter begin fun gl ->
end
end
-let fix ido n = match ido with
- | None ->
- Proofview.Goal.enter begin fun gl ->
- let name = Proof_global.get_current_proof_name () in
- let id = new_fresh_id Id.Set.empty name gl in
- mutual_fix id n [] 0
- end
- | Some id ->
- mutual_fix id n [] 0
+let fix id n = mutual_fix id n [] 0
let rec check_is_mutcoind env sigma cl =
let b = whd_all env sigma cl in
@@ -608,15 +606,7 @@ let mutual_cofix f others j = Proofview.Goal.enter begin fun gl ->
end
end
-let cofix ido = match ido with
- | None ->
- Proofview.Goal.enter begin fun gl ->
- let name = Proof_global.get_current_proof_name () in
- let id = new_fresh_id Id.Set.empty name gl in
- mutual_cofix id [] 0
- end
- | Some id ->
- mutual_cofix id [] 0
+let cofix id = mutual_cofix id [] 0
(**************************************************************)
(* Reduction and conversion tactics *)
@@ -965,6 +955,11 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
| LetIn (name,b,t,u) when not dep_flag || not (noccurn sigma 1 u) ->
let name = find_name false (LocalDef (name,b,t)) name_flag gl in
build_intro_tac name move_flag tac
+ | Evar ev when force_flag ->
+ let sigma, t = Evardefine.define_evar_as_product sigma ev in
+ Tacticals.New.tclTHEN
+ (Proofview.Unsafe.tclEVARS sigma)
+ (intro_then_gen name_flag move_flag force_flag dep_flag tac)
| _ ->
begin if not force_flag then Proofview.tclZERO (RefinerError (env, sigma, IntroNeedsProduct))
(* Note: red_in_concl includes betaiotazeta and this was like *)
@@ -1102,7 +1097,13 @@ let msg_quantified_hypothesis = function
pr_nth n ++
str " non dependent hypothesis"
+let warn_deprecated_intros_until_0 =
+ CWarnings.create ~name:"deprecated-intros-until-0" ~category:"tactics"
+ (fun () ->
+ strbrk"\"intros until 0\" is deprecated, use \"intros *\"; instead of \"induction 0\" and \"destruct 0\" use explicitly a name.\"")
+
let depth_of_quantified_hypothesis red h gl =
+ if h = AnonHyp 0 then warn_deprecated_intros_until_0 ();
match lookup_hypothesis_as_renamed_gen red h gl with
| Some depth -> depth
| None ->
@@ -1153,6 +1154,13 @@ let tactic_infer_flags with_evar = {
Pretyping.fail_evar = not with_evar;
Pretyping.expand_evars = true }
+type 'a core_destruction_arg =
+ | ElimOnConstr of 'a
+ | ElimOnIdent of lident
+ | ElimOnAnonHyp of int
+
+type 'a destruction_arg =
+ clear_flag * 'a core_destruction_arg
let onOpenInductionArg env sigma tac = function
| clear_flag,ElimOnConstr f ->
@@ -1245,7 +1253,6 @@ let cut c =
end
let error_uninstantiated_metas t clenv =
- let t = EConstr.Unsafe.to_constr t in
let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in
let id = match na with Name id -> id | _ -> anomaly (Pp.str "unnamed dependent meta.")
in user_err (str "Cannot find an instance for " ++ Id.print id ++ str".")
@@ -1255,7 +1262,7 @@ let check_unresolved_evars_of_metas sigma clenv =
(* Refiner.pose_all_metas_as_evars are resolved *)
List.iter (fun (mv,b) -> match b with
| Clval (_,(c,_),_) ->
- (match Constr.kind c.rebus with
+ (match Constr.kind (EConstr.Unsafe.to_constr c.rebus) with
| Evar (evk,_) when Evd.is_undefined clenv.evd evk
&& not (Evd.mem sigma evk) ->
error_uninstantiated_metas (mkMeta mv) clenv
@@ -1432,9 +1439,7 @@ let is_nonrec mind = (Global.lookup_mind (fst mind)).mind_finite == Declarations
let find_ind_eliminator ind s gl =
let gr = lookup_eliminator ind s in
- let evd, c = Tacmach.New.pf_apply Evd.fresh_global gl gr in
- let c = EConstr.of_constr c in
- evd, c
+ Tacmach.New.pf_apply Evd.fresh_global gl gr
let find_eliminator c gl =
let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_unsafe_type_of gl c) in
@@ -1958,24 +1963,22 @@ let on_the_bodies = function
exception DependsOnBody of Id.t option
let check_is_type env sigma ty =
- let evdref = ref sigma in
try
- let _ = Typing.e_sort_of env evdref ty in
- !evdref
+ let sigma, _ = Typing.sort_of env sigma ty in
+ sigma
with e when CErrors.noncritical e ->
raise (DependsOnBody None)
let check_decl env sigma decl =
let open Context.Named.Declaration in
let ty = NamedDecl.get_type decl in
- let evdref = ref sigma in
try
- let _ = Typing.e_sort_of env evdref ty in
- let _ = match decl with
- | LocalAssum _ -> ()
- | LocalDef (_,c,_) -> Typing.e_check env evdref c ty
+ let sigma, _ = Typing.sort_of env sigma ty in
+ let sigma = match decl with
+ | LocalAssum _ -> sigma
+ | LocalDef (_,c,_) -> Typing.check env sigma c ty
in
- !evdref
+ sigma
with e when CErrors.noncritical e ->
let id = NamedDecl.get_id decl in
raise (DependsOnBody (Some id))
@@ -2599,9 +2602,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
let eqdata = build_coq_eq_data () in
let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in
let (sigma, eq) = Evd.fresh_global env sigma eqdata.eq in
- let eq = EConstr.of_constr eq in
let (sigma, refl) = Evd.fresh_global env sigma eqdata.refl in
- let refl = EConstr.of_constr refl in
let eq = applist (eq,args) in
let refl = applist (refl, [t;mkVar id]) in
let term = mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)) in
@@ -2655,9 +2656,7 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
let eqdata = build_coq_eq_data () in
let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in
let (sigma, eq) = Evd.fresh_global env sigma eqdata.eq in
- let eq = EConstr.of_constr eq in
let (sigma, refl) = Evd.fresh_global env sigma eqdata.refl in
- let refl = EConstr.of_constr refl in
let eq = applist (eq,args) in
let refl = applist (refl, [t;mkVar id]) in
let newenv = insert_before [LocalAssum (heq,eq); decl] lastlhyp env in
@@ -2995,8 +2994,24 @@ let unfold_body x =
end
end
+let warn_cannot_remove_as_expected =
+ CWarnings.create ~name:"cannot-remove-as-expected" ~category:"tactics"
+ (fun (id,inglobal) ->
+ let pp = match inglobal with
+ | None -> mt ()
+ | Some ref -> str ", it is used implicitly in " ++ Printer.pr_global ref in
+ str "Cannot remove " ++ Id.print id ++ pp ++ str ".")
+
+let clear_for_destruct ids =
+ Proofview.tclORELSE
+ (clear_gen (fun env sigma id err inglobal -> raise (ClearDependencyError (id,err,inglobal))) ids)
+ (function
+ | ClearDependencyError (id,err,inglobal),_ -> warn_cannot_remove_as_expected (id,inglobal); Proofview.tclUNIT ()
+ | e -> iraise e)
+
(* Either unfold and clear if defined or simply clear if not a definition *)
-let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id]
+let expand_hyp id =
+ Tacticals.New.tclTRY (unfold_body id) <*> clear_for_destruct [id]
(*****************************)
(* High-level induction *)
@@ -3412,7 +3427,7 @@ let cook_sign hyp0_opt inhyps indvars env sigma =
type elim_scheme = {
elimc: constr with_bindings option;
elimt: types;
- indref: global_reference option;
+ indref: GlobRef.t option;
params: rel_context; (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
nparams: int; (* number of parameters *)
predicates: rel_context; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
@@ -3774,7 +3789,10 @@ let specialize_eqs id =
let ty = Tacmach.New.pf_get_hyp_typ id gl in
let evars = ref (Proofview.Goal.sigma gl) in
let unif env evars c1 c2 =
- compare_upto_variables !evars c1 c2 && Evarconv.e_conv env evars c1 c2
+ compare_upto_variables !evars c1 c2 &&
+ (match Evarconv.conv env !evars c1 c2 with
+ | Some sigma -> evars := sigma; true
+ | None -> false)
in
let rec aux in_eqs ctx acc ty =
match EConstr.kind !evars ty with
@@ -3799,7 +3817,8 @@ let specialize_eqs id =
| _ ->
if in_eqs then acc, in_eqs, ctx, ty
else
- let e = e_new_evar (push_rel_context ctx env) evars t in
+ let sigma, e = Evarutil.new_evar (push_rel_context ctx env) !evars t in
+ evars := sigma;
aux false (LocalDef (na,e,t) :: ctx) (mkApp (lift 1 acc, [| mkRel 1 |])) b)
| t -> acc, in_eqs, ctx, ty
in
@@ -4326,7 +4345,7 @@ let check_expected_type env sigma (elimc,bl) elimt =
let sigma,cl = make_evar_clause env sigma ~len:(n - 1) elimt in
let sigma = solve_evar_clause env sigma true cl bl in
let (_,u,_) = destProd sigma cl.cl_concl in
- fun t -> Evarconv.e_cumul env (ref sigma) t u
+ fun t -> Option.has_some (Evarconv.cumul env sigma t u)
let check_enough_applied env sigma elim =
(* A heuristic to decide whether the induction arg is enough applied *)
@@ -4917,9 +4936,9 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
let evd, ctx, concl =
(* FIXME: should be done only if the tactic succeeds *)
- let evd, nf = nf_evars_and_universes !evdref in
+ let evd = Evd.minimize_universes !evdref in
let ctx = Evd.universe_context_set evd in
- evd, ctx, nf concl
+ evd, ctx, Evarutil.nf_evars_universes evd concl
in
let concl = EConstr.of_constr concl in
let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac) in
@@ -4981,15 +5000,15 @@ let anon_id = Id.of_string "anonymous"
let name_op_to_name name_op object_kind suffix =
let open Proof_global in
let default_gk = (Global, false, object_kind) in
+ let name, gk = match Proof_global.V82.get_current_initial_conclusions () with
+ | (id, (_, gk)) -> Some id, gk
+ | exception NoCurrentProof -> None, default_gk
+ in
match name_op with
- | Some s ->
- (try let _, gk, _ = Pfedit.current_proof_statement () in s, gk
- with NoCurrentProof -> s, default_gk)
- | None ->
- let name, gk =
- try let name, gk, _ = Pfedit.current_proof_statement () in name, gk
- with NoCurrentProof -> anon_id, default_gk in
- add_suffix name suffix, gk
+ | Some s -> s, gk
+ | None ->
+ let name = Option.default anon_id name in
+ add_suffix name suffix, gk
let tclABSTRACT ?(opaque=true) name_op tac =
let s, gk = if opaque
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 079baa3efa..ddf78b1d4e 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -16,7 +16,6 @@ open Proof_type
open Evd
open Clenv
open Redexpr
-open Globnames
open Pattern
open Unification
open Misctypes
@@ -42,9 +41,9 @@ val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic
val convert_hyp_no_check : named_declaration -> unit Proofview.tactic
val mutual_fix :
Id.t -> int -> (Id.t * int * constr) list -> int -> unit Proofview.tactic
-val fix : Id.t option -> int -> unit Proofview.tactic
+val fix : Id.t -> int -> unit Proofview.tactic
val mutual_cofix : Id.t -> (Id.t * constr) list -> int -> unit Proofview.tactic
-val cofix : Id.t option -> unit Proofview.tactic
+val cofix : Id.t -> unit Proofview.tactic
val convert : constr -> constr -> unit Proofview.tactic
val convert_leq : constr -> constr -> unit Proofview.tactic
@@ -95,6 +94,14 @@ val try_intros_until :
(** Apply a tactic on a quantified hypothesis, an hypothesis in context
or a term with bindings *)
+type 'a core_destruction_arg =
+ | ElimOnConstr of 'a
+ | ElimOnIdent of lident
+ | ElimOnAnonHyp of int
+
+type 'a destruction_arg =
+ clear_flag * 'a core_destruction_arg
+
val onInductionArg :
(clear_flag -> constr with_bindings -> unit Proofview.tactic) ->
constr with_bindings destruction_arg -> unit Proofview.tactic
@@ -169,7 +176,7 @@ val change :
val pattern_option :
(occurrences * constr) list -> goal_location -> unit Proofview.tactic
val reduce : red_expr -> clause -> unit Proofview.tactic
-val unfold_constr : global_reference -> unit Proofview.tactic
+val unfold_constr : GlobRef.t -> unit Proofview.tactic
(** {6 Modification of the local context. } *)
@@ -245,7 +252,7 @@ val apply_delayed_in :
type elim_scheme = {
elimc: constr with_bindings option;
elimt: types;
- indref: global_reference option;
+ indref: GlobRef.t option;
params: rel_context; (** (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
nparams: int; (** number of parameters *)
predicates: rel_context; (** (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 753c608ada..6117999902 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -37,7 +37,7 @@ struct
type 't t =
| DRel
| DSort
- | DRef of global_reference
+ | DRef of GlobRef.t
| DCtx of 't * 't (* (binding list, subterm) = Prods and LetIns *)
| DLambda of 't * 't
| DApp of 't * 't (* binary app *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 06:50:03 +0000