From 9f723f14e5342c1303646b5ea7bb5c0012a090ef Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 4 Dec 2017 15:54:28 +0100 Subject: [econstr] Forbid calling `to_constr` in open terms. We forbid calling `EConstr.to_constr` on terms that are not evar-free, as to progress towards enforcing the invariant that `Constr.t` is evar-free. [c.f. #6308] Due to compatibility constraints we provide an optional parameter to `to_constr`, `abort` which can be used to overcome this restriction until we fix all parts of the code. Now, grepping for `~abort:false` should return the questionable parts of the system. Not a lot of places had to be fixed, some comments: - problems with the interface due to `Evd/Constr` [`Evd.define` being the prime example] do seem real! - inductives also look bad with regards to `Constr/EConstr`. - code in plugins needs work. A notable user of this "feature" is `Obligations/Program` that seem to like to generate kernel-level entries with free evars, then to scan them and workaround this problem by generating constants. --- .../06454-ejgallego-evar+strict_to_constr.sh | 8 ++++++++ engine/eConstr.ml | 16 +++++++++++----- engine/eConstr.mli | 13 ++++++++----- engine/evarutil.ml | 4 ++-- plugins/cc/cctac.ml | 2 +- plugins/firstorder/sequent.ml | 6 +++--- plugins/ssr/ssrcommon.ml | 2 +- plugins/ssr/ssrequality.ml | 11 +++++++---- plugins/ssr/ssripats.ml | 2 +- plugins/ssr/ssrview.ml | 2 +- pretyping/cases.ml | 3 ++- pretyping/evarsolve.ml | 4 ++-- pretyping/pretyping.ml | 4 ++-- pretyping/retyping.ml | 2 +- pretyping/tacred.ml | 2 +- pretyping/typing.ml | 6 +++--- pretyping/vnorm.ml | 4 ++-- tactics/hints.ml | 4 ++-- vernac/classes.ml | 2 +- vernac/comDefinition.ml | 4 ++-- vernac/comFixpoint.ml | 3 ++- vernac/comProgramFixpoint.ml | 8 +++++--- vernac/himsg.ml | 3 +-- 23 files changed, 69 insertions(+), 46 deletions(-) create mode 100644 dev/ci/user-overlays/06454-ejgallego-evar+strict_to_constr.sh 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 28c9dd3c2..dac937457 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 42566575c..8bba35440 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -410,7 +410,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 -- cgit v1.2.3