aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/user-overlays/06454-ejgallego-evar+strict_to_constr.sh8
-rw-r--r--engine/eConstr.ml16
-rw-r--r--engine/eConstr.mli13
-rw-r--r--engine/evarutil.ml4
-rw-r--r--plugins/cc/cctac.ml2
-rw-r--r--plugins/firstorder/sequent.ml6
-rw-r--r--plugins/ssr/ssrcommon.ml2
-rw-r--r--plugins/ssr/ssrequality.ml11
-rw-r--r--plugins/ssr/ssripats.ml2
-rw-r--r--plugins/ssr/ssrview.ml2
-rw-r--r--pretyping/cases.ml3
-rw-r--r--pretyping/evarsolve.ml4
-rw-r--r--pretyping/pretyping.ml4
-rw-r--r--pretyping/retyping.ml2
-rw-r--r--pretyping/tacred.ml2
-rw-r--r--pretyping/typing.ml6
-rw-r--r--pretyping/vnorm.ml4
-rw-r--r--tactics/hints.ml4
-rw-r--r--vernac/classes.ml2
-rw-r--r--vernac/comDefinition.ml4
-rw-r--r--vernac/comFixpoint.ml3
-rw-r--r--vernac/comProgramFixpoint.ml8
-rw-r--r--vernac/himsg.ml3
23 files changed, 69 insertions, 46 deletions
diff --git a/dev/ci/user-overlays/06454-ejgallego-evar+strict_to_constr.sh b/dev/ci/user-overlays/06454-ejgallego-evar+strict_to_constr.sh
new file mode 100644
index 000000000..f4cb71cf1
--- /dev/null
+++ b/dev/ci/user-overlays/06454-ejgallego-evar+strict_to_constr.sh
@@ -0,0 +1,8 @@
+if [ "$CI_PULL_REQUEST" = "6454" ] || [ "$CI_BRANCH" = "evar+strict_to_constr" ]; then
+
+ # ltac2_CI_BRANCH=econstr+more_fix
+ # ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+ Equations_CI_BRANCH=evar+strict_to_constr
+ Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+fi
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index bd47a04f1..01b4fe851 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -40,7 +40,7 @@ val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type
val whd_evar : Evd.evar_map -> t -> t
val of_kind : (t, t, ESorts.t, EInstance.t) Constr.kind_of_term -> t
val of_constr : Constr.t -> t
-val to_constr : evar_map -> t -> Constr.t
+val to_constr : ?abort_on_undefined_evars:bool -> evar_map -> t -> Constr.t
val unsafe_to_constr : t -> Constr.t
val unsafe_eq : (t, Constr.t) eq
val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, t) Context.Named.Declaration.pt
@@ -110,11 +110,16 @@ let of_constr c = c
let unsafe_to_constr c = c
let unsafe_eq = Refl
-let rec to_constr sigma c = match Constr.kind c with
+let to_constr ?(abort_on_undefined_evars=true) sigma c =
+let rec to_constr c = match Constr.kind c with
| Evar ev ->
begin match safe_evar_value sigma ev with
- | Some c -> to_constr sigma c
- | None -> Constr.map (fun c -> to_constr sigma c) c
+ | Some c -> to_constr c
+ | None ->
+ if abort_on_undefined_evars then
+ anomaly ~label:"econstr" Pp.(str "grounding a non evar-free term")
+ else
+ Constr.map (fun c -> to_constr c) c
end
| Sort (Sorts.Type u) ->
let u' = Evd.normalize_universe sigma u in
@@ -128,7 +133,8 @@ let rec to_constr sigma c = match Constr.kind c with
| Construct (co, u) when not (Univ.Instance.is_empty u) ->
let u' = Evd.normalize_universe_instance sigma u in
if u' == u then c else mkConstructU (co, u')
-| _ -> Constr.map (fun c -> to_constr sigma c) c
+| _ -> Constr.map (fun c -> to_constr c) c
+in to_constr c
let of_named_decl d = d
let unsafe_to_named_decl d = d
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 8ee3b9050..9cc9bf680 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -68,11 +68,14 @@ val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_ter
val kind_upto : Evd.evar_map -> Constr.t -> (Constr.t, Constr.t, Sorts.t, Univ.Instance.t) Constr.kind_of_term
-val to_constr : Evd.evar_map -> t -> Constr.t
-(** Returns the evar-normal form of the argument, and cast it as a theoretically
- evar-free term. In practice this function does not check that the result
- is actually evar-free, it is currently the duty of the caller to do so.
- This might change in the future. *)
+val to_constr : ?abort_on_undefined_evars:bool -> Evd.evar_map -> t -> Constr.t
+(** Returns the evar-normal form of the argument. Note that this
+ function is supposed to be called when the original term has not
+ more free-evars anymore. If you need compatibility with the old
+ semantics, set [abort_on_undefined_evars] to [false].
+
+ For getting the evar-normal form of a term with evars see
+ {!Evarutil.nf_evar}. *)
val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 45760c6b4..c707b37b6 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -72,9 +72,9 @@ let flush_and_check_evars sigma c =
(** Term exploration up to instantiation. *)
let kind_of_term_upto = EConstr.kind_upto
-let nf_evar0 sigma t = EConstr.to_constr sigma (EConstr.of_constr t)
+let nf_evar0 sigma t = EConstr.to_constr ~abort_on_undefined_evars:false sigma (EConstr.of_constr t)
let whd_evar = EConstr.whd_evar
-let nf_evar sigma c = EConstr.of_constr (EConstr.to_constr sigma c)
+let nf_evar sigma c = EConstr.of_constr (EConstr.to_constr ~abort_on_undefined_evars:false sigma c)
let j_nf_evar sigma j =
{ uj_val = nf_evar sigma j.uj_val;
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index d19817e74..c4db49cd3 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -90,7 +90,7 @@ let rec decompose_term env sigma t=
decompose_term env sigma c
| _ ->
let t = Termops.strip_outer_cast sigma t in
- if closed0 sigma t then Symb (EConstr.to_constr sigma t) else raise Not_found
+ if closed0 sigma t then Symb (EConstr.to_constr ~abort_on_undefined_evars:false sigma t) else raise Not_found
(* decompose equality in members and type *)
open Termops
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 285991797..83fbc2d5d 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -77,14 +77,14 @@ module CM=Map.Make(Constr)
module History=Set.Make(Hitem)
let cm_add sigma typ nam cm=
- let typ = EConstr.to_constr sigma typ in
+ let typ = EConstr.to_constr ~abort_on_undefined_evars:false sigma typ in
try
let l=CM.find typ cm in CM.add typ (nam::l) cm
with
Not_found->CM.add typ [nam] cm
let cm_remove sigma typ nam cm=
- let typ = EConstr.to_constr sigma typ in
+ let typ = EConstr.to_constr ~abort_on_undefined_evars:false sigma typ in
try
let l=CM.find typ cm in
let l0=List.filter (fun id-> not (Globnames.eq_gr id nam)) l in
@@ -152,7 +152,7 @@ let re_add_formula_list sigma lf seq=
redexes=List.fold_right HP.add lf seq.redexes;
context=List.fold_right do_one lf seq.context}
-let find_left sigma t seq=List.hd (CM.find (EConstr.to_constr sigma t) seq.context)
+let find_left sigma t seq=List.hd (CM.find (EConstr.to_constr ~abort_on_undefined_evars:false sigma t) seq.context)
(*let rev_left seq=
try
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index d5118da4c..e07bc48a4 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -504,7 +504,7 @@ let nf_evar sigma t =
EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr t))
let pf_abs_evars2 gl rigid (sigma, c0) =
- let c0 = EConstr.to_constr sigma c0 in
+ let c0 = EConstr.to_constr ~abort_on_undefined_evars:false sigma c0 in
let sigma0, ucst = project gl, Evd.evar_universe_context sigma in
let nenv = env_size (pf_env gl) in
let abs_evar n k =
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 57635edac..2f0433b64 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -276,7 +276,7 @@ let unfoldintac occ rdx t (kt,_) gl =
let foldtac occ rdx ft gl =
let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in
let sigma, t = ft in
- let t = EConstr.to_constr sigma t in
+ let t = EConstr.to_constr ~abort_on_undefined_evars:false sigma t in
let fold, conclude = match rdx with
| Some (_, (In_T _ | In_X_In_T _)) | None ->
let ise = Evd.create_evar_defs sigma in
@@ -557,7 +557,7 @@ let rwrxtac occ rdx_pat dir rule gl =
let rpat env sigma0 (sigma, pats) (d, r, lhs, rhs) =
let sigma, pat =
let rw_progress rhs t evd = rw_progress rhs (EConstr.of_constr t) evd in
- mk_tpattern env sigma0 (sigma,EConstr.to_constr sigma r) (rw_progress rhs) d (EConstr.to_constr sigma lhs) in
+ mk_tpattern env sigma0 (sigma, EConstr.to_constr ~abort_on_undefined_evars:false sigma r) (rw_progress rhs) d (EConstr.to_constr ~abort_on_undefined_evars:false sigma lhs) in
sigma, pats @ [pat] in
let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in
let find_R, end_R = mk_tpattern_matcher sigma0 occ ~upats_origin rpats in
@@ -567,7 +567,7 @@ let rwrxtac occ rdx_pat dir rule gl =
let r = ref None in
(fun env c _ h -> do_once r (fun () -> find_rule (EConstr.of_constr c), c); mkRel h),
(fun concl -> closed0_check concl e gl;
- let (d,(ev,ctx,c)) , x = assert_done r in (d,(ev,ctx, EConstr.to_constr ev c)) , x) in
+ let (d,(ev,ctx,c)) , x = assert_done r in (d,(ev,ctx, EConstr.to_constr ~abort_on_undefined_evars:false ev c)) , x) in
let concl0 = EConstr.Unsafe.to_constr concl0 in
let concl = eval_pattern env0 sigma0 concl0 rdx_pat occ find_R in
let (d, r), rdx = conclude concl in
@@ -589,7 +589,10 @@ let ssrinstancesofrule ist dir arg gl =
let rpat env sigma0 (sigma, pats) (d, r, lhs, rhs) =
let sigma, pat =
let rw_progress rhs t evd = rw_progress rhs (EConstr.of_constr t) evd in
- mk_tpattern env sigma0 (sigma,EConstr.to_constr sigma r) (rw_progress rhs) d (EConstr.to_constr sigma lhs) in
+ mk_tpattern env sigma0
+ (sigma,EConstr.to_constr ~abort_on_undefined_evars:false sigma r)
+ (rw_progress rhs) d
+ (EConstr.to_constr ~abort_on_undefined_evars:false sigma lhs) in
sigma, pats @ [pat] in
let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in
mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true sigma0 None ~upats_origin rpats in
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 7897cb170..af78bf36a 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -418,7 +418,7 @@ let tclLAST_GEN ~to_ind ((oclr, occ), t) conclusion = tclINDEPENDENTL begin
Goal.enter_one begin fun g ->
let pat = Ssrmatching.interp_cpattern sigma0 t None in
let cl0, env, sigma, hyps = Goal.(concl g, env g, sigma g, hyps g) in
- let cl = EConstr.to_constr sigma cl0 in
+ let cl = EConstr.to_constr ~abort_on_undefined_evars:false sigma cl0 in
let (c, ucst), cl =
try Ssrmatching.fill_occ_pattern ~raise_NoMatch:true env sigma cl pat occ 1
with Ssrmatching.NoMatch -> Ssrmatching.redex_of_pattern env pat, cl in
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index aa614fbc1..afe03533d 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -254,7 +254,7 @@ let finalize_view s0 ?(simple_types=true) p =
Goal.enter_one ~__LOC__ begin fun g ->
let env = Goal.env g in
let sigma = Goal.sigma g in
- let evars_of_p = Evd.evars_of_term (EConstr.to_constr sigma p) in
+ let evars_of_p = Evd.evars_of_term (EConstr.to_constr ~abort_on_undefined_evars:false sigma p) in
let filter x _ = Evar.Set.mem x evars_of_p in
let sigma = Typeclasses.resolve_typeclasses ~fail:false ~filter env sigma in
let p = Reductionops.nf_evar sigma p in
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 73be9d6b7..b16f1a9ed 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2581,7 +2581,8 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar
let body = it_mkLambda_or_LetIn (applist (j.uj_val, args)) lets in
let j =
{ uj_val = it_mkLambda_or_LetIn body tomatchs_lets;
- uj_type = EConstr.of_constr (EConstr.to_constr !evdref tycon); }
+ (* XXX: is this normalization needed? *)
+ uj_type = Evarutil.nf_evar !evdref tycon; }
in j
(**************************************************************************)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 96d80741a..0c109b026 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1592,14 +1592,14 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
Id.Set.subset (collect_vars evd rhs) !names
in
let body =
- if fast rhs then EConstr.of_constr (EConstr.to_constr evd rhs) (** FIXME? *)
+ if fast rhs then nf_evar evd rhs (** FIXME? *)
else
let t' = imitate (env,0) rhs in
if !progress then
(recheck_applications conv_algo (evar_env evi) evdref t'; t')
else t'
in (!evdref,body)
-
+
(* [define] tries to solve the problem "?ev[args] = rhs" when "?ev" is
* an (uninstantiated) evar such that "hyps |- ?ev : typ". Otherwise said,
* [define] tries to find an instance lhs such that
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 4962b89a0..2c371d5cf 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -117,7 +117,7 @@ open ExtraEnv
exception Found of int array
let nf_fix sigma (nas, cs, ts) =
- let inj c = EConstr.to_constr sigma c in
+ let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in
(nas, Array.map inj cs, Array.map inj ts)
let search_guard ?loc env possible_indexes fixdefs =
@@ -1150,7 +1150,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match D
(* Correction of bug #5315 : we need to define an evar for *all* holes *)
let evkt = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s) in
let ev,_ = destEvar !evdref evkt in
- evdref := Evd.define ev (to_constr !evdref v) !evdref;
+ evdref := Evd.define ev (to_constr ~abort_on_undefined_evars:false !evdref v) !evdref;
(* End of correction of bug #5315 *)
{ utj_val = v;
utj_type = s }
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 3582b6447..95aa5ebef 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -170,7 +170,7 @@ let retype ?(polyprop=true) sigma =
and type_of_global_reference_knowing_parameters env c args =
let argtyps =
- Array.map (fun c -> lazy (EConstr.to_constr sigma (type_of env c))) args in
+ Array.map (fun c -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma (type_of env c))) args in
match EConstr.kind sigma c with
| Ind (ind, u) ->
let u = EInstance.kind sigma u in
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 518d2f604..977713fd8 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -558,7 +558,7 @@ let match_eval_ref_value env sigma constr stack =
else
None
| Proj (p, c) when not (Projection.unfolded p) ->
- reduction_effect_hook env sigma (EConstr.to_constr sigma constr)
+ reduction_effect_hook env sigma (EConstr.to_constr ~abort_on_undefined_evars:false sigma constr)
(lazy (EConstr.to_constr sigma (applist (constr,stack))));
if is_evaluable env (EvalConstRef (Projection.constant p)) then
Some (mkProj (Projection.unfold p, c))
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 4c834f2f8..c4eb6af89 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -35,7 +35,7 @@ let meta_type evd mv =
let inductive_type_knowing_parameters env sigma (ind,u) jl =
let u = Unsafe.to_instance u in
let mspec = lookup_mind_specif env ind in
- let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr sigma j.uj_type)) jl in
+ let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma j.uj_type)) jl in
Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp
let e_type_judgment env evdref j =
@@ -155,7 +155,7 @@ let e_type_case_branches env evdref (ind,largs) pj c =
let p = pj.uj_val in
let params = List.map EConstr.Unsafe.to_constr params in
let () = e_is_correct_arity env evdref c pj ind specif params in
- let lc = build_branches_type ind specif params (EConstr.to_constr !evdref p) in
+ let lc = build_branches_type ind specif params (EConstr.to_constr ~abort_on_undefined_evars:false !evdref p) in
let lc = Array.map EConstr.of_constr lc in
let n = (snd specif).Declarations.mind_nrealdecls in
let ty = whd_betaiota !evdref (lambda_applist_assum !evdref (n+1) p (realargs@[c])) in
@@ -207,7 +207,7 @@ let enrich_env env evdref =
Environ.env_of_pre_env penv'
let check_fix env sigma pfix =
- let inj c = EConstr.to_constr sigma c in
+ let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in
let (idx, (ids, cs, ts)) = pfix in
check_fix env (idx, (ids, Array.map inj cs, Array.map inj ts))
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 3c9b8bc33..f314ae0d6 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -381,8 +381,8 @@ let cbv_vm env sigma c t =
if Termops.occur_meta sigma c then
CErrors.user_err Pp.(str "vm_compute does not support metas.");
(** This evar-normalizes terms beforehand *)
- let c = EConstr.to_constr sigma c in
- let t = EConstr.to_constr sigma t in
+ let c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in
+ let t = EConstr.to_constr ~abort_on_undefined_evars:false sigma t in
let v = Vconv.val_of_constr env c in
EConstr.of_constr (nf_val env sigma v t)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index a285d6b93..46d162911 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -792,7 +792,7 @@ let make_exact_entry env sigma info poly ?(name=PathAny) (c, cty, ctx) =
match EConstr.kind sigma cty with
| Prod _ -> failwith "make_exact_entry"
| _ ->
- let pat = Patternops.pattern_of_constr env sigma (EConstr.to_constr sigma cty) in
+ let pat = Patternops.pattern_of_constr env sigma (EConstr.to_constr ~abort_on_undefined_evars:false sigma cty) in
let hd =
try head_pattern_bound pat
with BoundPattern -> failwith "make_exact_entry"
@@ -814,7 +814,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) info poly ?(name=PathAny) (c
let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
let ce = mk_clenv_from_env env sigma' None (c,cty) in
let c' = clenv_type (* ~reduce:false *) ce in
- let pat = Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma c') in
+ let pat = Patternops.pattern_of_constr env ce.evd (EConstr.to_constr ~abort_on_undefined_evars:false sigma c') in
let hd =
try head_pattern_bound pat
with BoundPattern -> failwith "make_apply_entry" in
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 76d427add..3c133f317 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -293,7 +293,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
(* Check that the type is free of evars now. *)
Pretyping.check_evars env Evd.empty sigma termtype;
let termtype = to_constr sigma termtype in
- let term = Option.map (to_constr sigma) term in
+ let term = Option.map (to_constr ~abort_on_undefined_evars:false sigma) term in
if not (Evd.has_undefined sigma) && not (Option.is_empty term) then
declare_instance_constant k pri global imps ?hook id decl
poly sigma (Option.get term) termtype
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index b18a60a1f..9aa61ab46 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -88,8 +88,8 @@ let interp_definition pl bl poly red_option c ctypopt =
let evd = Evd.minimize_universes evd in
(* Substitute evars and universes, and add parameters.
Note: in program mode some evars may remain. *)
- let ctx = List.map (EConstr.to_rel_decl evd) ctx in
- let c = Term.it_mkLambda_or_LetIn (EConstr.to_constr evd c) ctx in
+ let ctx = List.map Termops.(map_rel_decl (to_constr ~abort_on_undefined_evars:false evd)) ctx in
+ let c = Term.it_mkLambda_or_LetIn (EConstr.to_constr ~abort_on_undefined_evars:false evd c) ctx in
let tyopt = Option.map (fun ty -> Term.it_mkProd_or_LetIn (EConstr.to_constr evd ty) ctx) tyopt in
(* Keep only useful universes. *)
let uvars_fold uvars c =
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index a794c2db0..1466fa243 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -225,7 +225,8 @@ let interp_recursive ~program_mode ~cofix fixl notations =
(* Instantiate evars and check all are resolved *)
let sigma = solve_unif_constraints_with_heuristics env_rec sigma in
let sigma, _ = nf_evars_and_universes sigma in
- let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr sigma) c) fixdefs in
+ (* XXX: We still have evars here in Program *)
+ let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr ~abort_on_undefined_evars:false sigma) c) fixdefs in
let fixtypes = List.map EConstr.(to_constr sigma) fixtypes in
let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index b95741ca4..745f1df1d 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -229,7 +229,8 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
in
(* XXX: Capturing sigma here... bad bad *)
let hook = Lemmas.mk_hook (hook sigma) in
- let fullcoqc = EConstr.to_constr sigma def in
+ (* XXX: Grounding non-ground terms here... bad bad *)
+ let fullcoqc = EConstr.to_constr ~abort_on_undefined_evars:false sigma def in
let fullctyp = EConstr.to_constr sigma typ in
Obligations.check_evars env sigma;
let evars, _, evars_def, evars_typ =
@@ -261,9 +262,10 @@ let do_program_recursive local poly fixkind fixl ntns =
let collect_evars id def typ imps =
(* Generalize by the recursive prototypes *)
let def =
- EConstr.to_constr evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign)
+ EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign)
and typ =
- EConstr.to_constr evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign)
+ (* Worrying... *)
+ EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign)
in
let evm = collect_evars_of_term evd def typ in
let evars, _, def, typ =
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 698ee4703..23c863cab 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -640,8 +640,7 @@ let explain_refiner_cannot_generalize env sigma ty =
pr_leconstr_env env sigma ty ++ str "."
let explain_no_occurrence_found env sigma c id =
- let c = EConstr.to_constr sigma c in
- str "Found no subterm matching " ++ pr_lconstr_env env sigma c ++
+ str "Found no subterm matching " ++ pr_leconstr_env env sigma c ++
str " in " ++
(match id with
| Some id -> Id.print id
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 15:21:12 +0000