aboutsummaryrefslogtreecommitdiffhomepage
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.ml4
-rw-r--r--tactics/class_tactics.ml45
-rw-r--r--tactics/contradiction.ml2
-rw-r--r--tactics/eauto.ml11
-rw-r--r--tactics/elimschemes.ml4
-rw-r--r--tactics/eqdecide.ml2
-rw-r--r--tactics/eqschemes.ml34
-rw-r--r--tactics/equality.ml54
-rw-r--r--tactics/hints.ml133
-rw-r--r--tactics/hints.mli66
-rw-r--r--tactics/hipattern.ml8
-rw-r--r--tactics/hipattern.mli2
-rw-r--r--tactics/ind_tables.ml4
-rw-r--r--tactics/inv.ml8
-rw-r--r--tactics/leminv.ml2
-rw-r--r--tactics/tacticals.ml21
-rw-r--r--tactics/tacticals.mli6
-rw-r--r--tactics/tactics.ml142
-rw-r--r--tactics/tactics.mli11
-rw-r--r--tactics/term_dnet.ml4
-rw-r--r--tactics/term_dnet.mli2
23 files changed, 302 insertions, 274 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 0c0d9bcfc..77fe31415 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 c3857e6b8..0b0e629ab 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 8e50c977e..aca7f6c65 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -9,7 +9,7 @@
(************************************************************************)
open Util
-open Term
+open Constr
open EConstr
open Names
open Pattern
@@ -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 0260460e6..c105116ff 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -18,6 +18,7 @@ open CErrors
open Util
open Names
open Term
+open Constr
open Termops
open EConstr
open Tacmach
@@ -226,7 +227,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
@@ -546,12 +547,7 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
let hints = build_subclasses ~check:false env sigma (VarRef id) empty_hint_info in
(List.map_append
(fun (path,info,c) ->
- let info =
- { info with Vernacexpr.hint_pattern =
- Option.map (Constrintern.intern_constr_pattern env sigma)
- info.Vernacexpr.hint_pattern }
- in
- make_resolves env sigma ~name:(PathHints path)
+ make_resolves env sigma ~name:(PathHints path)
(true,false,not !Flags.quiet) info false
(IsConstr (EConstr.of_constr c,Univ.ContextSet.empty)))
hints)
@@ -653,17 +649,6 @@ module Search = struct
Evd.add sigma gl evi')
sigma goals
- let fail_if_nonclass info =
- Proofview.Goal.enter begin fun gl ->
- let sigma = Proofview.Goal.sigma gl in
- if is_class_type sigma (Proofview.Goal.concl gl) then
- Proofview.tclUNIT ()
- else (if !typeclasses_debug > 1 then
- Feedback.msg_debug (pr_depth info.search_depth ++
- str": failure due to non-class subgoal " ++
- pr_ev sigma (Proofview.Goal.goal gl));
- Proofview.tclZERO NoApplicableEx) end
-
(** The general hint application tactic.
tac1 + tac2 .... The choice of OR or ORELSE is determined
depending on the dependencies of the goal and the unique/Prop
@@ -802,13 +787,8 @@ module Search = struct
in
if path_matches derivs [] then aux e tl
else
- let filter =
- if false (* in 8.6, still allow non-class subgoals
- info.search_only_classes *) then fail_if_nonclass info
- else Proofview.tclUNIT ()
- in
ortac
- (with_shelf (tac <*> filter) >>= fun s ->
+ (with_shelf tac >>= fun s ->
let i = !idx in incr idx; result s i None)
(fun e' ->
if CErrors.noncritical (fst e') then
@@ -872,12 +852,9 @@ module Search = struct
let search_tac_gl ?st only_classes dep hints depth i sigma gls gl :
unit Proofview.tactic =
let open Proofview in
- if false (* In 8.6, still allow non-class goals only_classes && not (is_class_type sigma (Goal.concl gl)) *) then
- Tacticals.New.tclZEROMSG (str"Not a subgoal for a class")
- else
- let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in
- let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in
- search_tac hints depth 1 info
+ let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in
+ let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in
+ search_tac hints depth 1 info
let search_tac ?(st=full_transparent_state) only_classes dep hints depth =
let open Proofview in
@@ -1030,8 +1007,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 +1053,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 +1151,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/contradiction.ml b/tactics/contradiction.ml
index c285f21e7..b92bc75bc 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -8,7 +8,7 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Term
+open Constr
open EConstr
open Hipattern
open Tactics
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index dc310c542..80d07c5c0 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -12,7 +12,7 @@ open Pp
open CErrors
open Util
open Names
-open Term
+open Constr
open Termops
open EConstr
open Proof_type
@@ -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 6bd4866c6..70f73df5c 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/eqdecide.ml b/tactics/eqdecide.ml
index b0deeed17..176701d99 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -17,7 +17,7 @@
open Util
open Names
open Namegen
-open Term
+open Constr
open EConstr
open Declarations
open Tactics
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 477de6452..eede13329 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 75b76695c..d7e697aed 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -15,6 +15,7 @@ open Util
open Names
open Nameops
open Term
+open Constr
open Termops
open EConstr
open Vars
@@ -1108,8 +1109,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 +1177,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 +1215,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 +1372,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 +1760,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 +1782,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 +1833,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/hints.ml b/tactics/hints.ml
index a285d6b93..4b77418ff 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -12,7 +12,7 @@ open Pp
open Util
open CErrors
open Names
-open Term
+open Constr
open Evd
open EConstr
open Vars
@@ -23,17 +23,16 @@ open Libobject
open Namegen
open Libnames
open Smartlocate
-open Misctypes
open Termops
open Inductiveops
open Typing
open Decl_kinds
+open Typeclasses
open Pattern
open Patternops
open Clenv
open Tacred
open Printer
-open Vernacexpr
module NamedDecl = Context.Named.Declaration
@@ -94,13 +93,14 @@ let secvars_of_hyps hyps =
else pred
let empty_hint_info =
- let open Vernacexpr in
{ hint_priority = None; hint_pattern = None }
(************************************************************************)
(* The Type of Constructions Autotactic Hints *)
(************************************************************************)
+type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen
+
type 'a hint_ast =
| Res_pf of 'a (* Hint Apply *)
| ERes_pf of 'a (* Hint EApply *)
@@ -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,9 +153,27 @@ 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 reference_or_constr =
+ | HintsReference of reference
+ | HintsConstr of Constrexpr.constr_expr
+
+type hint_mode =
+ | ModeInput (* No evars *)
+ | ModeNoHeadEvar (* No evar at the head *)
+ | ModeOutput (* Anything *)
+
+type hints_expr =
+ | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
+ | HintsImmediate of reference_or_constr list
+ | HintsUnfold of reference list
+ | HintsTransparency of reference list * bool
+ | HintsMode of reference * hint_mode list
+ | HintsConstructors of reference list
+ | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
+
type import_level = [ `LAX | `WARN | `STRICT ]
let warn_hint : import_level ref = ref `LAX
@@ -276,15 +294,15 @@ let strip_params env sigma c =
| App (f, args) ->
(match EConstr.kind sigma f with
| Const (p,_) ->
- let cb = lookup_constant p env in
- (match cb.Declarations.const_proj with
- | Some pb ->
- let n = pb.Declarations.proj_npars in
- if Array.length args > n then
- mkApp (mkProj (Projection.make p false, args.(n)),
- Array.sub args (n+1) (Array.length args - (n + 1)))
- else c
- | None -> c)
+ let p = Projection.make p false in
+ (match lookup_projection p env with
+ | pb ->
+ let n = pb.Declarations.proj_npars in
+ if Array.length args > n then
+ mkApp (mkProj (p, args.(n)),
+ Array.sub args (n+1) (Array.length args - (n + 1)))
+ else c
+ | exception Not_found -> c)
| _ -> c)
| _ -> c
@@ -308,7 +326,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 +383,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 +466,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 +492,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 +528,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 +672,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.filter p sdl
let remove_he st p se =
let sl1' = remove_sdl p se.sentry_nopat in
@@ -664,9 +682,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.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 +810,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 +832,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 +894,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 +1033,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 +1083,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 +1122,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
@@ -1218,7 +1236,7 @@ let add_trivials env sigma l local dbnames =
type hnf = bool
-type hint_info = (patvar list * constr_pattern) hint_info_gen
+type nonrec hint_info = hint_info
type hints_entry =
| HintsResolveEntry of (hint_info * polymorphic * hnf * hints_path_atom * hint_term) list
@@ -1226,7 +1244,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 +1281,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 +1296,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;
@@ -1322,7 +1344,7 @@ let interp_hints poly =
let _, tacexp = Genintern.generic_intern env tacexp in
HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp)
-let add_hints local dbnames0 h =
+let add_hints ~local dbnames0 h =
if String.List.mem "nocore" dbnames0 then
user_err Pp.(str "The hint database \"nocore\" is meant to stay empty.");
let dbnames = if List.is_empty dbnames0 then ["core"] else dbnames0 in
@@ -1357,12 +1379,10 @@ let expand_constructor_hints env sigma lems =
(* builds a hint database from a constr signature *)
(* typically used with (lid, ltyp) = pf_hyps_types <some goal> *)
-let add_hint_lemmas env sigma eapply lems hint_db =
+let constructor_hints env sigma eapply lems =
let lems = expand_constructor_hints env sigma lems in
- let hintlist' =
- List.map_append (fun (poly, lem) ->
- make_resolves env sigma (eapply,true,false) empty_hint_info poly lem) lems in
- Hint_db.add_list env sigma hintlist' hint_db
+ List.map_append (fun (poly, lem) ->
+ make_resolves env sigma (eapply,true,false) empty_hint_info poly lem) lems
let make_local_hint_db env sigma ts eapply lems =
let map c = c env sigma in
@@ -1373,8 +1393,9 @@ let make_local_hint_db env sigma ts eapply lems =
| Some ts -> ts
in
let hintlist = List.map_append (make_resolve_hyp env sigma) sign in
- add_hint_lemmas env sigma eapply lems
- (Hint_db.add_list env sigma hintlist (Hint_db.empty ts false))
+ Hint_db.empty ts false
+ |> Hint_db.add_list env sigma hintlist
+ |> Hint_db.add_list env sigma (constructor_hints env sigma eapply lems)
let make_local_hint_db env sigma ?ts eapply lems =
make_local_hint_db env sigma ts eapply lems
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 1811150c2..7ef7f0185 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -12,29 +12,29 @@ open Util
open Names
open EConstr
open Environ
-open Globnames
open Decl_kinds
open Evd
-open Misctypes
open Tactypes
open Clenv
open Pattern
-open Vernacexpr
+open Typeclasses
(** {6 General functions. } *)
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 *)
+type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen
+
type 'a hint_ast =
| Res_pf of 'a (* Hint Apply *)
| ERes_pf of 'a (* Hint EApply *)
@@ -51,7 +51,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 {
@@ -72,6 +72,24 @@ type search_entry
type hint_entry
+type reference_or_constr =
+ | HintsReference of Libnames.reference
+ | HintsConstr of Constrexpr.constr_expr
+
+type hint_mode =
+ | ModeInput (* No evars *)
+ | ModeNoHeadEvar (* No evar at the head *)
+ | ModeOutput (* Anything *)
+
+type hints_expr =
+ | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
+ | HintsImmediate of reference_or_constr list
+ | HintsUnfold of Libnames.reference list
+ | HintsTransparency of Libnames.reference list * bool
+ | HintsMode of Libnames.reference * hint_mode list
+ | HintsConstructors of Libnames.reference list
+ | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
+
type 'a hints_path_gen =
| PathAtom of 'a hints_path_atom_gen
| PathStar of 'a hints_path_gen
@@ -81,7 +99,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 +109,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 +125,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 +162,8 @@ type hint_db = Hint_db.t
type hnf = bool
-type hint_info = (patvar list * constr_pattern) 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 +173,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 +187,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
@@ -179,7 +195,7 @@ val current_pure_db : unit -> hint_db list
val interp_hints : polymorphic -> hints_expr -> hints_entry
-val add_hints : locality_flag -> hint_db_name list -> hints_entry -> unit
+val add_hints : local:bool -> hint_db_name list -> hints_entry -> unit
val prepare_hint : bool (* Check no remaining evars *) ->
(bool * bool) (* polymorphic or monomorphic, local or global *) ->
@@ -264,7 +280,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
@@ -274,3 +290,5 @@ val pr_hint : env -> evar_map -> hint -> Pp.t
(** Hook for changing the initialization of auto *)
val add_hints_init : (unit -> unit) -> unit
+type nonrec hint_info = hint_info
+[@@ocaml.deprecated "Use [Typeclasses.hint_info]"]
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index b012a7ecd..5d264058a 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -12,7 +12,7 @@ open Pp
open CErrors
open Util
open Names
-open Term
+open Constr
open Termops
open EConstr
open Inductiveops
@@ -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 0697d0f19..f04cda123 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 62ead57f3..21520f5d2 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 590098bdc..339abbc2e 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -14,6 +14,7 @@ open Util
open Names
open Term
open Termops
+open Constr
open EConstr
open Vars
open Namegen
@@ -124,12 +125,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
@@ -294,7 +293,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
@@ -498,9 +497,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/leminv.ml b/tactics/leminv.ml
index a4cdc1592..f47e6b2cd 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -12,9 +12,9 @@ open Pp
open CErrors
open Util
open Names
-open Term
open Termops
open Environ
+open Constr
open EConstr
open Vars
open Namegen
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index a97ae8f65..732d06f8a 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
@@ -492,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 *)
@@ -506,8 +508,8 @@ 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
- | Term.Evar (evk,l) -> is_undefined_up_to_restriction sigma evk
+ | Evd.Evar_defined c -> match Constr.kind (EConstr.Unsafe.to_constr c) with
+ | Evar (evk,l) -> is_undefined_up_to_restriction sigma evk
| _ ->
(* We make the assumption that there is no way to refine an
evar remaining after typing from the initial term given to
@@ -709,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 ->
@@ -769,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 340d8fbf3..cbaf691f1 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 *)
@@ -223,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
@@ -268,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 d0ec3358a..58c62af85 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -128,14 +128,14 @@ let unsafe_intro env store decl b =
(sigma, mkNamedLambda_or_LetIn decl ev)
end
-let introduction ?(check=true) id =
+let introduction id =
Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let sigma = Tacmach.New.project gl in
let hyps = named_context_val (Proofview.Goal.env gl) in
let store = Proofview.Goal.extra gl in
let env = Proofview.Goal.env gl in
- let () = if check && mem_named_context_val id hyps then
+ let () = if mem_named_context_val id hyps then
user_err ~hdr:"Tactics.introduction"
(str "Variable " ++ Id.print id ++ str " is already declared.")
in
@@ -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 *)
@@ -1258,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".")
@@ -1268,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
@@ -1445,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
@@ -1918,8 +1910,8 @@ let cast_no_check cast c =
exact_no_check (mkCast (c, cast, concl))
end
-let vm_cast_no_check c = cast_no_check Term.VMcast c
-let native_cast_no_check c = cast_no_check Term.NATIVEcast c
+let vm_cast_no_check c = cast_no_check VMcast c
+let native_cast_no_check c = cast_no_check NATIVEcast c
let exact_proof c =
let open Tacmach.New in
@@ -1971,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))
@@ -2612,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
@@ -2668,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
@@ -3008,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 *)
@@ -3425,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,...) *)
@@ -3787,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
@@ -3812,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
@@ -4339,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 *)
@@ -4930,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
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 7809dbf48..b17330f13 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
@@ -35,16 +34,16 @@ val is_quantified_hypothesis : Id.t -> Proofview.Goal.t -> bool
(** {6 Primitive tactics. } *)
-val introduction : ?check:bool -> Id.t -> unit Proofview.tactic
+val introduction : Id.t -> unit Proofview.tactic
val convert_concl : ?check:bool -> types -> cast_kind -> unit Proofview.tactic
val convert_hyp : ?check:bool -> named_declaration -> unit Proofview.tactic
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
@@ -177,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. } *)
@@ -253,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 753c608ad..8bdcc6321 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 *)
@@ -290,7 +290,7 @@ struct
| Const (c,u) -> Term (DRef (ConstRef c))
| Ind (i,u) -> Term (DRef (IndRef i))
| Construct (c,u)-> Term (DRef (ConstructRef c))
- | Term.Meta _ -> assert false
+ | Meta _ -> assert false
| Evar (i,_) ->
let meta =
try Evar.Map.find i !metas
diff --git a/tactics/term_dnet.mli b/tactics/term_dnet.mli
index 2c748f9c9..7bce57789 100644
--- a/tactics/term_dnet.mli
+++ b/tactics/term_dnet.mli
@@ -26,7 +26,7 @@ open Mod_subst
The results returned here are perfect, since post-filtering is done
inside here.
- See lib/dnet.mli for more details.
+ See tactics/dnet.mli for more details.
*)
(** Identifiers to store (right hand side of the association) *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 14:35:15 +0000