aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/db2
-rw-r--r--dev/doc/changes.txt5
-rw-r--r--plugins/subtac/subtac_cases.ml6
-rw-r--r--plugins/subtac/subtac_classes.ml4
-rw-r--r--plugins/subtac/subtac_coercion.ml4
-rw-r--r--plugins/subtac/subtac_command.ml12
-rw-r--r--plugins/subtac/subtac_pretyping.ml2
-rw-r--r--pretyping/cases.ml2
-rw-r--r--pretyping/evarconv.ml10
-rw-r--r--pretyping/evarutil.ml74
-rw-r--r--pretyping/evarutil.mli23
-rw-r--r--pretyping/unification.ml4
-rw-r--r--tactics/rewrite.ml48
-rw-r--r--tactics/tactics.ml8
-rw-r--r--test-suite/success/replace.v8
-rw-r--r--toplevel/classes.ml6
-rw-r--r--toplevel/command.ml6
-rw-r--r--toplevel/lemmas.ml2
18 files changed, 94 insertions, 92 deletions
diff --git a/dev/db b/dev/db
index ca5c27de3b..6be2c20b92 100644
--- a/dev/db
+++ b/dev/db
@@ -6,8 +6,6 @@ install_printer Top_printers.ppidset
install_printer Top_printers.ppevarsubst
install_printer Top_printers.ppintset
install_printer Top_printers.pplab
-install_printer Top_printers.ppmsid
-install_printer Top_printers.ppmbid
install_printer Top_printers.ppdir
install_printer Top_printers.ppmp
install_printer Top_printers.ppkn
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 784283358a..1321b49785 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -17,6 +17,11 @@ generally fewer than the defined ones.
= CHANGES BETWEEN COQ V8.2 AND COQ V8.3 =
=========================================
+** Light cleaning in evarutil.ml **
+
+whd_castappevar is now whd_head_evar
+obsolete whd_ise disappears
+
** Semantical change of h_induction_destruct **
Warning, the order of the isrec and evar_flag was inconsistent and has
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 29ce9d3d4a..491b44fbba 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -1894,7 +1894,7 @@ let liftn_rel_context n k sign =
liftrec (k + rel_context_length sign) sign
let nf_evars_env sigma (env : env) : env =
- let nf t = nf_isevar sigma t in
+ let nf t = nf_evar sigma t in
let env0 : env = reset_context env in
let f e (na, b, t) e' : env =
Environ.push_named (na, Option.map nf b, nf t) e'
@@ -1912,7 +1912,7 @@ let prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs sign tycon
match rtntyp with
| Some rtntyp ->
let predcclj = typing_fun (mk_tycon (new_Type ())) newenv rtntyp in
- let predccl = (j_nf_isevar !isevars predcclj).uj_val in
+ let predccl = (j_nf_evar !isevars predcclj).uj_val in
Some (build_initial_predicate true allnames predccl)
| None ->
match valcon_of_tycon tycon with
@@ -1993,7 +1993,7 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra
let body = it_mkLambda_or_LetIn (applistc j.uj_val args) lets in
let j =
{ uj_val = it_mkLambda_or_LetIn body tomatchs_lets;
- uj_type = nf_isevar !isevars tycon; }
+ uj_type = nf_evar !isevars tycon; }
in j
else
(* We build the elimination predicate if any and check its consistency *)
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 4a254d7910..2fe22364d5 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -164,8 +164,8 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
let term = Termops.it_mkLambda_or_LetIn def ctx in
term, termtype
in
- let termtype = Evarutil.nf_isevar !evars termtype in
- let term = Evarutil.nf_isevar !evars term in
+ let termtype = Evarutil.nf_evar !evars termtype in
+ let term = Evarutil.nf_evar !evars term in
evars := undefined_evars !evars;
Evarutil.check_evars env Evd.empty !evars termtype;
let hook vis gr =
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index 1bc3dbb345..3c907962ce 100644
--- a/plugins/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
@@ -456,8 +456,8 @@ module Coercion = struct
let (evd', val') =
try
inh_conv_coerce_to_fail loc env evd rigidonly
- (Some (nf_isevar evd cj.uj_val))
- (nf_isevar evd cj.uj_type) (nf_isevar evd t)
+ (Some (nf_evar evd cj.uj_val))
+ (nf_evar evd cj.uj_type) (nf_evar evd t)
with NoCoercion ->
let sigma = evd in
try
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 8a7d11d1d8..d93a4b695e 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -50,7 +50,7 @@ open Subtac_obligations
(* Functions to parse and interpret constructions *)
let evar_nf isevars c =
- Evarutil.nf_isevar !isevars c
+ Evarutil.nf_evar !isevars c
let interp_gen kind isevars env
?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
@@ -213,7 +213,7 @@ let telescope = function
let nf_evar_context isevars ctx =
List.map (fun (n, b, t) ->
- (n, Option.map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx
+ (n, Option.map (Evarutil.nf_evar isevars) b, Evarutil.nf_evar isevars t)) ctx
let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
Coqlib.check_required_library ["Coq";"Program";"Wf"];
@@ -318,7 +318,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
let _ = isevars := Evarutil.nf_evar_map !isevars in
let binders_rel = nf_evar_context !isevars binders_rel in
let binders = nf_evar_context !isevars binders in
- let top_arity = Evarutil.nf_isevar !isevars top_arity in
+ let top_arity = Evarutil.nf_evar !isevars top_arity in
let hook, recname, typ =
if List.length binders_rel > 1 then
let name = add_suffix recname "_func" in
@@ -326,7 +326,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
let body = it_mkLambda_or_LetIn (mkApp (constr_of_global gr, [|make|])) binders_rel in
let ty = it_mkProd_or_LetIn top_arity binders_rel in
let ce =
- { const_entry_body = Evarutil.nf_isevar !isevars body;
+ { const_entry_body = Evarutil.nf_evar !isevars body;
const_entry_type = Some ty;
const_entry_opaque = false;
const_entry_boxed = false}
@@ -345,8 +345,8 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
Impargs.declare_manual_implicits false gr impls
in hook, recname, typ
in
- let fullcoqc = Evarutil.nf_isevar !isevars def in
- let fullctyp = Evarutil.nf_isevar !isevars typ in
+ let fullcoqc = Evarutil.nf_evar !isevars def in
+ let fullctyp = Evarutil.nf_evar !isevars typ in
let evm = evars_of_term !isevars Evd.empty fullctyp in
let evm = evars_of_term !isevars evm fullcoqc in
let evm = non_instanciated_map env isevars evm in
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index a59cb96652..5b42c8ba5f 100644
--- a/plugins/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.ml
@@ -125,7 +125,7 @@ let subtac_process env isevars id bl c tycon =
let imps = Option.default (Implicit_quantifiers.implicits_of_rawterm ~with_products:false c) imps in
let coqc, ctyp = interp env isevars c tycon in
let evm = non_instanciated_map env isevars !isevars in
- let ty = nf_isevar !isevars (match tycon with Some (None, c) -> c | _ -> ctyp) in
+ let ty = nf_evar !isevars (match tycon with Some (None, c) -> c | _ -> ctyp) in
evm, coqc, ty, imps
open Subtac_obligations
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index aa0f4843fa..da417f44df 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1655,7 +1655,7 @@ let prepare_predicate loc typing_fun evdref env tomatchs sign tycon pred =
evdref :=
Coercion.inh_conv_coerces_to loc env !evdref predcclj.uj_val tycon)
tycon;
- let predccl = (j_nf_isevar !evdref predcclj).uj_val in
+ let predccl = (j_nf_evar !evdref predcclj).uj_val in
[!evdref, KnownDep, predccl]
in
List.map
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 486fd05b3d..3a236671ab 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -159,8 +159,8 @@ let ise_array2 evd f v1 v2 =
let rec evar_conv_x env evd pbty term1 term2 =
let sigma = evd in
- let term1 = whd_castappevar sigma term1 in
- let term2 = whd_castappevar sigma term2 in
+ let term1 = whd_head_evar sigma term1 in
+ let term2 = whd_head_evar sigma term2 in
(* Maybe convertible but since reducing can erase evars which [evar_apprec]
could have found, we do it only if the terms are free of evar.
Note: incomplete heuristic... *)
@@ -187,7 +187,7 @@ let rec evar_conv_x env evd pbty term1 term2 =
(decompose_app term1) (decompose_app term2)
and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
- (* Evar must be undefined since we have whd_ised *)
+ (* Evar must be undefined since we have flushed evars *)
match (flex_kind_of_term term1 l1, flex_kind_of_term term2 l2) with
| Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
let f1 i =
@@ -521,8 +521,8 @@ let choose_less_dependent_instance evk evd term args =
Evd.define evk (mkVar (fst (List.hd subst'))) evd
let apply_conversion_problem_heuristic env evd pbty t1 t2 =
- let t1 = apprec_nohdbeta env evd (whd_castappevar evd t1) in
- let t2 = apprec_nohdbeta env evd (whd_castappevar evd t2) in
+ let t1 = apprec_nohdbeta env evd (whd_head_evar evd t1) in
+ let t2 = apprec_nohdbeta env evd (whd_head_evar evd t2) in
let (term1,l1 as appr1) = decompose_app t1 in
let (term2,l2 as appr2) = decompose_app t2 in
match kind_of_term term1, kind_of_term term2 with
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index e104fe9083..c7258ccfeb 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -21,33 +21,18 @@ open Reductionops
open Pretype_errors
open Retyping
-(* Expanding existential variables (pretyping.ml) *)
-(* 1- whd_ise fails if an existential is undefined *)
+(* Expanding existential variables *)
+(* 1- flush_and_check_evars fails if an existential is undefined *)
exception Uninstantiated_evar of existential_key
-let rec whd_ise sigma c =
+let rec flush_and_check_evars sigma c =
match kind_of_term c with
- | Evar (evk,_ as ev) when Evd.is_defined sigma evk ->
- whd_ise sigma (existential_value sigma ev)
- | Evar (evk,_) when Evd.is_undefined sigma evk ->
- raise (Uninstantiated_evar evk)
- | _ -> c
-
-
-(* Expand evars, possibly in the head of an application *)
-let whd_castappevar_stack sigma c =
- let rec whrec (c, l as s) =
- match kind_of_term c with
- | Evar (evk,args as ev) when Evd.is_defined sigma evk
- -> whrec (existential_value sigma ev, l)
- | Cast (c,_,_) -> whrec (c, l)
- | App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
- | _ -> s
- in
- whrec (c, [])
-
-let whd_castappevar sigma c = applist (whd_castappevar_stack sigma c)
+ | Evar (evk,_ as ev) ->
+ (match existential_opt_value sigma ev with
+ | None -> raise (Uninstantiated_evar evk)
+ | Some c -> flush_and_check_evars sigma c)
+ | _ -> map_constr (flush_and_check_evars sigma) c
let nf_evar = Pretype_errors.nf_evar
let j_nf_evar = Pretype_errors.j_nf_evar
@@ -79,12 +64,6 @@ let nf_evars evm = Evd.fold (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info ev
let nf_evar_map evd = Evd.evars_reset_evd (nf_evars evd) evd
-let nf_isevar evd = nf_evar evd
-let j_nf_isevar evd = j_nf_evar evd
-let jl_nf_isevar evd = jl_nf_evar evd
-let jv_nf_isevar evd = jv_nf_evar evd
-let tj_nf_isevar evd = tj_nf_evar evd
-
(**********************)
(* Creating new metas *)
(**********************)
@@ -1177,6 +1156,8 @@ let is_ground_env evd env =
structures *)
let is_ground_env = memo1_2 is_ground_env
+(* Return the head evar if any *)
+
exception NoHeadEvar
let head_evar =
@@ -1189,6 +1170,22 @@ let head_evar =
in
hrec
+(* Expand head evar if any (currently consider only applications but I
+ guess it should consider Case too) *)
+
+let whd_head_evar_stack sigma c =
+ let rec whrec (c, l as s) =
+ match kind_of_term c with
+ | Evar (evk,args as ev) when Evd.is_defined sigma evk
+ -> whrec (existential_value sigma ev, l)
+ | Cast (c,_,_) -> whrec (c, l)
+ | App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
+ | _ -> s
+ in
+ whrec (c, [])
+
+let whd_head_evar sigma c = applist (whd_head_evar_stack sigma c)
+
(* Check if an applied evar "?X[args] l" is a Miller's pattern; note
that we don't care whether args itself contains Rel's or even Rel's
distinct from the ones in l *)
@@ -1338,10 +1335,10 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1)
let evi = Evd.find evd evk1 in
if occur_existential evd evi.evar_concl then
let evenv = evar_unfiltered_env evi in
- let evc = nf_isevar evd evi.evar_concl in
+ let evc = nf_evar evd evi.evar_concl in
match evi.evar_body with
| Evar_defined body ->
- let ty = nf_isevar evd (Retyping.get_type_of evenv evd body) in
+ let ty = nf_evar evd (Retyping.get_type_of evenv evd body) in
add_conv_pb (Reduction.CUMUL,evenv,ty,evc) evd
| Evar_empty -> (* Resulted in a constraint *)
evd
@@ -1379,18 +1376,17 @@ let evars_of_evar_info evi =
(evars_of_named_context (named_context_of_val evi.evar_hyps)))
(* [check_evars] fails if some unresolved evar remains *)
-(* it assumes that the defined existentials have already been substituted *)
-let check_evars env initial_sigma evd c =
- let sigma = evd in
- let c = nf_evar sigma c in
+let check_evars env initial_sigma sigma c =
let rec proc_rec c =
match kind_of_term c with
- | Evar (evk,args) ->
- assert (Evd.mem sigma evk);
+ | Evar (evk,_ as ev) ->
+ (match existential_opt_value sigma ev with
+ | Some c -> proc_rec c
+ | None ->
if not (Evd.mem initial_sigma evk) then
- let (loc,k) = evar_source evk evd in
- (match k with
+ let (loc,k) = evar_source evk sigma in
+ match k with
| ImplicitArg (gr, (i, id), false) -> ()
| _ ->
let evi = nf_evar_info sigma (Evd.find_undefined sigma evk) in
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 1d11097d30..e47d452b00 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -69,9 +69,13 @@ val non_instantiated : evar_map -> (evar * evar_info) list
(**********************************************************
Unification utils *)
+(** [head_evar c} returns the head evar of [c] if any *)
exception NoHeadEvar
val head_evar : constr -> existential_key (** may raise NoHeadEvar *)
+(* Expand head evar if any *)
+val whd_head_evar : evar_map -> constr -> constr
+
val is_ground_term : evar_map -> constr -> bool
val is_ground_env : evar_map -> env -> bool
val solve_refl :
@@ -132,8 +136,8 @@ val lift_tycon : int -> type_constraint -> type_constraint
(***********************************************************)
-(** [whd_ise] raise [Uninstantiated_evar] if an evar remains uninstantiated;
- *[whd_evar]* and *[nf_evar]* leave uninstantiated evar as is *)
+(** [flush_and_check_evars] raise [Uninstantiated_evar] if an evar remains
+ uninstantiated; [nf_evar] leaves uninstantiated evars as is *)
val nf_evar : evar_map -> constr -> constr
val j_nf_evar : evar_map -> unsafe_judgment -> unsafe_judgment
@@ -151,22 +155,11 @@ val nf_named_context_evar : evar_map -> named_context -> named_context
val nf_rel_context_evar : evar_map -> rel_context -> rel_context
val nf_env_evar : evar_map -> env -> env
-(** Same for evar defs *)
-val nf_isevar : evar_map -> constr -> constr
-val j_nf_isevar : evar_map -> unsafe_judgment -> unsafe_judgment
-val jl_nf_isevar :
- evar_map -> unsafe_judgment list -> unsafe_judgment list
-val jv_nf_isevar :
- evar_map -> unsafe_judgment array -> unsafe_judgment array
-val tj_nf_isevar :
- evar_map -> unsafe_type_judgment -> unsafe_type_judgment
-
val nf_evar_map : evar_map -> evar_map
-(** Replacing all evars *)
+(** Replacing all evars, possibly raising [Uninstantiated_evar] *)
exception Uninstantiated_evar of existential_key
-val whd_ise : evar_map -> constr -> constr
-val whd_castappevar : evar_map -> constr -> constr
+val flush_and_check_evars : evar_map -> constr -> constr
(** Replace the vars and rels that are aliases to other vars and rels by
their representative that is most ancient in the context *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 411dc0da6a..a2a37edfc8 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -221,8 +221,8 @@ let oracle_order env cf1 cf2 =
let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flags m n =
let rec unirec_rec (curenv,nb as curenvnb) pb b ((sigma,metasubst,evarsubst) as substn) curm curn =
- let cM = Evarutil.whd_castappevar sigma curm
- and cN = Evarutil.whd_castappevar sigma curn in
+ let cM = Evarutil.whd_head_evar sigma curm
+ and cN = Evarutil.whd_head_evar sigma curn in
match (kind_of_term cM,kind_of_term cN) with
| Meta k1, Meta k2 ->
let stM,stN = extract_instance_status pb in
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 12a14eb014..a0d0027e42 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1006,12 +1006,12 @@ let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl =
let cstrevars = !evars in
let evars = solve_constraints env cstrevars in
let p = map_rewprf
- (fun p -> nf_zeta env evars (Evarutil.nf_isevar evars p))
+ (fun p -> nf_zeta env evars (Evarutil.nf_evar evars p))
p
in
- let newt = Evarutil.nf_isevar evars newt in
+ let newt = Evarutil.nf_evar evars newt in
let abs = Option.map (fun (x, y) ->
- Evarutil.nf_isevar evars x, Evarutil.nf_isevar evars y) abs in
+ Evarutil.nf_evar evars x, Evarutil.nf_evar evars y) abs in
let undef = split_evars (fst cstrevars) evars in
let rewtac =
match is_hyp with
@@ -1422,7 +1422,7 @@ let build_morphism_signature m =
mkApp (Lazy.force proper_type, [| t; sig_; m |])
in
let evd = solve_constraints env !isevars in
- let m = Evarutil.nf_isevar evd morph in
+ let m = Evarutil.nf_evar evd morph in
Evarutil.check_evars env Evd.empty evd m; m
let default_morphism sign m =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0be1e08fc6..9f5c611234 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2470,7 +2470,7 @@ let specialize_eqs id gl =
let acc' = it_mkLambda_or_LetIn acc ctx'' in
let ty' = Tacred.whd_simpl env !evars ty'
and acc' = Tacred.whd_simpl env !evars acc' in
- let ty' = Evarutil.nf_isevar !evars ty' in
+ let ty' = Evarutil.nf_evar !evars ty' in
if worked then
tclTHENFIRST (Tacmach.internal_cut true id ty')
(exact_no_check (refresh_universes_strict acc')) gl
@@ -3463,8 +3463,10 @@ let abstract_subproof id tac gl =
global_sign (empty_named_context,empty_named_context_val) in
let id = next_global_ident_away id (pf_ids_of_hyps gl) in
let concl = it_mkNamedProd_or_LetIn (pf_concl gl) sign in
- if occur_existential concl then
- error "\"abstract\" cannot handle existentials.";
+ let concl =
+ try flush_and_check_evars (project gl) concl
+ with Uninstantiated_evar _ ->
+ error "\"abstract\" cannot handle existentials." in
let const = Pfedit.build_constant_by_tactic secsign concl
(tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)) in
let cd = Entries.DefinitionEntry const in
diff --git a/test-suite/success/replace.v b/test-suite/success/replace.v
index 6acdd51616..0b112937e5 100644
--- a/test-suite/success/replace.v
+++ b/test-suite/success/replace.v
@@ -22,3 +22,11 @@ replace x with 0 in H,H0 |- * .
Undo.
Admitted.
+(* This failed at some point when "replace" started to support arguments
+ with evars but "abstract" did not supported any evars even defined ones *)
+
+Class U.
+Lemma l (u : U) (f : U -> nat) (H : 0 = f u) : f u = 0.
+replace (f _) with 0 by abstract apply H.
+reflexivity.
+Qed.
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index d161470245..62a7ebb445 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -184,7 +184,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
let _, ty_constr = instance_constructor k (List.rev subst) in
let termtype =
let t = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
- Evarutil.nf_isevar !evars t
+ Evarutil.nf_evar !evars t
in
Evarutil.check_evars env Evd.empty !evars termtype;
let cst = Declare.declare_internal_constant id
@@ -249,8 +249,8 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
let term = Termops.it_mkLambda_or_LetIn def ctx in
term, termtype
in
- let termtype = Evarutil.nf_isevar !evars termtype in
- let term = Evarutil.nf_isevar !evars term in
+ let termtype = Evarutil.nf_evar !evars termtype in
+ let term = Evarutil.nf_evar !evars term in
let evm = undefined_evars !evars in
Evarutil.check_evars env Evd.empty !evars termtype;
if Evd.is_empty evm then
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 8d840a4580..4259ccb81c 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -73,7 +73,7 @@ let interp_definition boxed bl red_option c ctypopt =
match ctypopt with
None ->
let c, imps2 = interp_constr_evars_impls ~evdref ~fail_evar:false env_bl c in
- let body = nf_isevar !evdref (it_mkLambda_or_LetIn c ctx) in
+ let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in
check_evars env Evd.empty !evdref body;
imps1@imps2,
{ const_entry_body = body;
@@ -83,8 +83,8 @@ let interp_definition boxed bl red_option c ctypopt =
| Some ctyp ->
let ty, impls = interp_type_evars_impls ~evdref ~fail_evar:false env_bl ctyp in
let c, imps2 = interp_casted_constr_evars_impls ~evdref ~fail_evar:false env_bl c ty in
- let body = nf_isevar !evdref (it_mkLambda_or_LetIn c ctx) in
- let typ = nf_isevar !evdref (it_mkProd_or_LetIn ty ctx) in
+ let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in
+ let typ = nf_evar !evdref (it_mkProd_or_LetIn ty ctx) in
check_evars env Evd.empty !evdref body;
check_evars env Evd.empty !evdref typ;
imps1@imps2,
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 01cfd22e81..efb0595ab6 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -320,7 +320,7 @@ let start_proof_com kind thms hook =
Sign.iter_rel_context (check_evars env Evd.empty !evdref) ctx;
let ids = List.map pi1 ctx in
(compute_proof_name (fst kind) sopt,
- (nf_isevar !evdref (it_mkProd_or_LetIn t' ctx),
+ (nf_evar !evdref (it_mkProd_or_LetIn t' ctx),
(ids, imps @ lift_implicits (List.length ids) imps'),
guard)))
thms in
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-01 23:22:15 +0000