aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/evarutil.ml13
-rw-r--r--engine/evarutil.mli15
-rw-r--r--plugins/ssr/ssrcommon.ml5
-rw-r--r--pretyping/evarconv.ml5
-rw-r--r--pretyping/evarsolve.ml11
-rw-r--r--pretyping/globEnv.ml3
-rw-r--r--proofs/clenv.ml3
-rw-r--r--tactics/tactics.ml10
8 files changed, 22 insertions, 43 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 9bfe3e21f3..b4b2032dd2 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -436,14 +436,6 @@ let new_pure_evar ?(src=default_source) ?(filter = Filter.identity) ?(abstract_a
in
(evd, newevk)
-let new_evar_instance ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate
- ?principal sign evd typ instance =
- let open EConstr in
- assert (not !Flags.debug ||
- List.distinct (ids_of_named_context (named_context_of_val sign)));
- let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate ?principal typ in
- evd, mkEvar (newevk, instance)
-
(* [new_evar] declares a new existential in an env env with type typ *)
(* Converting the env into the sign of the evar to define *)
let new_evar ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate
@@ -455,8 +447,9 @@ let new_evar ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_can
match filter with
| None -> instance
| Some filter -> Filter.filter_list filter instance in
- new_evar_instance sign evd typ' ?src ?filter ?abstract_arguments ?candidates ?naming
- ?typeclass_candidate ?principal instance
+ let (evd, evk) = new_pure_evar sign evd typ' ?src ?filter ?abstract_arguments ?candidates ?naming
+ ?typeclass_candidate ?principal in
+ (evd, EConstr.mkEvar (evk, instance))
let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid =
let (evd', s) = new_sort_variable rigid evd in
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index c592a4f5d1..41b58d38b0 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -63,21 +63,6 @@ val new_Type : ?rigid:rigid -> evar_map -> evar_map * constr
val new_global : evar_map -> GlobRef.t -> evar_map * constr
-(** Create a fresh evar in a context different from its definition context:
- [new_evar_instance sign evd ty inst] creates a new evar of context
- [sign] and type [ty], [inst] is a mapping of the evar context to
- the context where the evar should occur. This means that the terms
- of [inst] are typed in the occurrence context and their type (seen
- as a telescope) is [sign] *)
-val new_evar_instance :
- ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
- ?abstract_arguments:Abstraction.t -> ?candidates:constr list ->
- ?naming:intro_pattern_naming_expr ->
- ?typeclass_candidate:bool ->
- ?principal:bool ->
- named_context_val -> evar_map -> types ->
- constr list -> evar_map * constr
-
val make_pure_subst : evar_info -> 'a list -> (Id.t * 'a) list
val safe_evar_value : evar_map -> Constr.existential -> Constr.constr option
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 5f463f8de4..65204b7868 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1351,9 +1351,8 @@ let unsafe_intro env decl b =
let inst = List.map (get_id %> EConstr.mkVar) (Environ.named_context env) in
let ninst = EConstr.mkRel 1 :: inst in
let nb = EConstr.Vars.subst1 (EConstr.mkVar (get_id decl)) b in
- let sigma, ev =
- Evarutil.new_evar_instance nctx sigma nb ~principal:true ninst in
- sigma, EConstr.mkNamedLambda_or_LetIn decl ev
+ let sigma, ev = Evarutil.new_pure_evar ~principal:true nctx sigma nb in
+ sigma, EConstr.mkNamedLambda_or_LetIn decl (EConstr.mkEvar (ev, ninst))
end
let set_decl_id id = let open Context in function
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 6880383a31..400acc25b6 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1411,11 +1411,10 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
refresh_universes ~status:Evd.univ_flexible (Some true)
env_evar_unf evd evty
else evd, evty in
- let (evd, ev) = new_evar_instance sign evd evty ~filter instance in
- let evk = fst (destEvar evd ev) in
+ let (evd, evk) = new_pure_evar sign evd evty ~filter in
evsref := (evk,evty,inst,prefer_abstraction)::!evsref;
fixed := Evar.Set.add evk !fixed;
- evd, ev
+ evd, mkEvar (evk, instance)
in
let evd, rhs' = apply_on_subterm env_rhs evd fixed set_var test c rhs in
if debug_ho_unification () then
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 348d7c0b2f..79839099f7 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -698,10 +698,9 @@ let make_projectable_subst aliases sigma evi args =
*)
let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_sign sign filter inst_in_env =
- let (evd, evar_in_env) = new_evar_instance sign evd ty_t_in_sign ~filter ~src inst_in_env in
+ let (evd, evk) = new_pure_evar sign evd ty_t_in_sign ~filter ~src in
let t_in_env = whd_evar evd t_in_env in
- let (evk, _) = destEvar evd evar_in_env in
- let evd = define_fun env evd None (destEvar evd evar_in_env) t_in_env in
+ let evd = define_fun env evd None (evk, inst_in_env) t_in_env in
let ctxt = named_context_of_val sign in
let inst_in_sign = inst_of_vars (Filter.filter_list filter ctxt) in
let evar_in_sign = mkEvar (evk, inst_in_sign) in
@@ -770,9 +769,9 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
define_evar_from_virtual_equation define_fun env evd src ty_in_env
ty_t_in_sign sign2 filter2 inst2_in_env in
let (evd, ev2_in_sign) =
- new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 ~src inst2_in_sign in
- let ev2_in_env = (fst (destEvar evd ev2_in_sign), inst2_in_env) in
- (evd, ev2_in_sign, ev2_in_env)
+ new_pure_evar sign2 evd ev2ty_in_sign ~filter:filter2 ~src in
+ let ev2_in_env = (ev2_in_sign, inst2_in_env) in
+ (evd, mkEvar (ev2_in_sign, inst2_in_sign), ev2_in_env)
let restrict_upon_filter evd evk p args =
let oldfullfilter = evar_filter (Evd.find_undefined evd evk) in
diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
index 05abb86f46..81a62a7048 100644
--- a/pretyping/globEnv.ml
+++ b/pretyping/globEnv.ml
@@ -110,7 +110,8 @@ let new_evar env sigma ?src ?naming typ =
let instance = rel_list (nb_rel env.renamed_env) inst_vars in
let (subst, _, sign) = Lazy.force env.extra in
let typ' = csubst_subst subst typ in
- new_evar_instance sign sigma typ' ?src ?naming instance
+ let (sigma, evk) = new_pure_evar sign sigma typ' ?src ?naming in
+ (sigma, mkEvar (evk, instance))
let new_type_evar env sigma ~src =
let sigma, s = Evd.new_sort_variable Evd.univ_flexible_alg sigma in
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 4d148756b4..9bd7ccda5d 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -781,7 +781,8 @@ let make_evar_clause env sigma ?len t =
Some (ctx, args, subst), ctx, args, subst
| Some (ctx, args, subst) -> inst, ctx, args, subst
in
- let (sigma, ev) = new_evar_instance ~typeclass_candidate:false ctx sigma (csubst_subst subst t1) args in
+ let (sigma, ev) = new_pure_evar ~typeclass_candidate:false ctx sigma (csubst_subst subst t1) in
+ let ev = mkEvar (ev, args) in
let dep = not (noccurn sigma 1 t2) in
let hole = {
hole_evar = ev;
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7269b5c02d..f553a290f9 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -120,8 +120,8 @@ let unsafe_intro env decl b =
let inst = List.map (NamedDecl.get_id %> mkVar) (named_context env) in
let ninst = mkRel 1 :: inst in
let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in
- let (sigma, ev) = new_evar_instance nctx sigma nb ~principal:true ninst in
- (sigma, mkLambda_or_LetIn (NamedDecl.to_rel_decl decl) ev)
+ let (sigma, ev) = new_pure_evar nctx sigma nb ~principal:true in
+ (sigma, mkLambda_or_LetIn (NamedDecl.to_rel_decl decl) (mkEvar (ev, ninst)))
end
let introduction id =
@@ -340,7 +340,8 @@ let rename_hyp repl =
let nctx = val_of_named_context nhyps in
let instance = List.map (NamedDecl.get_id %> mkVar) hyps in
Refine.refine ~typecheck:false begin fun sigma ->
- Evarutil.new_evar_instance nctx sigma nconcl ~principal:true instance
+ let sigma, ev = Evarutil.new_pure_evar nctx sigma nconcl ~principal:true in
+ sigma, mkEvar (ev, instance)
end
end
@@ -438,7 +439,8 @@ let clear_hyps2 env sigma ids sign t cl =
let new_evar_from_context ?principal sign evd typ =
let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in
- Evarutil.new_evar_instance sign evd typ instance
+ let (evd, evk) = Evarutil.new_pure_evar sign evd typ in
+ (evd, mkEvar (evk, instance))
let internal_cut ?(check=true) replace id t =
Proofview.Goal.enter begin fun gl ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:41:59 +0000