From 3a0b543af4ac99b29efdebe27b1d204d044a7bf0 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 31 Mar 2018 17:43:18 +0200 Subject: Evar maps contain econstrs. We bootstrap the circular evar_map <-> econstr dependency by moving the internal EConstr.API module to Evd.MiniEConstr. Then we make the Evd functions use econstr. --- plugins/firstorder/sequent.ml | 2 +- plugins/funind/functional_principles_proofs.ml | 3 +-- plugins/funind/functional_principles_types.ml | 15 +++++++++------ plugins/funind/glob_termops.ml | 7 ++++--- plugins/funind/indfun.ml | 11 +++-------- plugins/funind/invfun.ml | 8 ++------ plugins/ltac/extratactics.ml4 | 2 -- plugins/ltac/rewrite.ml | 8 ++++---- plugins/ssr/ssrcommon.ml | 16 +++++++++------- plugins/ssr/ssrelim.ml | 2 +- plugins/ssr/ssrequality.ml | 6 +++--- plugins/ssr/ssripats.ml | 2 +- plugins/ssr/ssrview.ml | 2 +- plugins/ssrmatching/ssrmatching.ml4 | 24 ++++++++++++++---------- 14 files changed, 53 insertions(+), 55 deletions(-) (limited to 'plugins') diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 83fbc2d5d..7c612c0d8 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -197,7 +197,7 @@ let extend_with_ref_list env sigma l seq = let l = expand_constructor_hints l in let f gr (seq, sigma) = let sigma, c = Evd.fresh_global env sigma gr in - let sigma, typ= Typing.type_of env sigma (EConstr.of_constr c) in + let sigma, typ= Typing.type_of env sigma c in (add_formula env sigma Hyp gr typ seq, sigma) in List.fold_right f l (seq, sigma) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index d04887a48..8da0e1c4f 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1050,8 +1050,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a (Global.env ()) !evd (Constrintern.locate_reference (qualid_of_ident equation_lemma_id)) in - let res = EConstr.of_constr res in - evd:=evd'; + evd:=evd'; let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd res in res in diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 804548ce5..04a23cdb9 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -266,7 +266,7 @@ let change_property_sort evd toSort princ princName = (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident princName)) in let init = let nargs = (princ_info.nparams + (List.length princ_info.predicates)) in - mkApp(princName_as_constr, + mkApp(EConstr.Unsafe.to_constr princName_as_constr, Array.init nargs (fun i -> mkRel (nargs - i ))) in @@ -630,11 +630,14 @@ let build_scheme fas = in let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in let _ = evd := evd' in - let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr f) in - if isConst f - then (destConst f,sort) - else user_err Pp.(pr_constr_env (Global.env ()) !evd f ++spc () ++ str "should be the named of a globally defined function") - ) + let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd f in + let c, u = + try EConstr.destConst !evd f + with DestKO -> + user_err Pp.(pr_econstr_env (Global.env ()) !evd f ++spc () ++ str "should be the named of a globally defined function") + in + (c, EConstr.EInstance.kind !evd u), sort + ) fas ) in let bodies_types = diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 40ea40b6b..845104c3c 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -564,6 +564,7 @@ let resolve_and_replace_implicits ?(flags=Pretyping.all_and_fail_flags) ?(expect If someone knows how to prevent solved existantial removal in understand, please do not hesitate to change the computation of [ctx] here *) let ctx,_,_ = Pretyping.ise_pretype_gen flags env sigma Glob_ops.empty_lvar expected_type rt in let ctx, f = Evarutil.nf_evars_and_universes ctx in + let f c = EConstr.of_constr (f (EConstr.Unsafe.to_constr c)) in (* then we map [rt] to replace the implicit holes by their values *) let rec change rt = @@ -586,8 +587,8 @@ If someone knows how to prevent solved existantial removal in understand, pleas with Found evi -> (* we found the evar corresponding to this hole *) match evi.evar_body with | Evar_defined c -> - (* we just have to lift the solution in glob_term *) - Detyping.detype Detyping.Now false Id.Set.empty env ctx (EConstr.of_constr (f c)) + (* we just have to lift the solution in glob_term *) + Detyping.detype Detyping.Now false Id.Set.empty env ctx (f c) | Evar_empty -> rt (* the hole was not solved : we do nothing *) ) | (GHole(BinderType na,_,_)) -> (* we only want to deal with implicit arguments *) @@ -609,7 +610,7 @@ If someone knows how to prevent solved existantial removal in understand, pleas match evi.evar_body with | Evar_defined c -> (* we just have to lift the solution in glob_term *) - Detyping.detype Detyping.Now false Id.Set.empty env ctx (EConstr.of_constr (f c)) + Detyping.detype Detyping.Now false Id.Set.empty env ctx (f c) | Evar_empty -> rt (* the hole was not solved : we d when falseo nothing *) in res diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d395e3601..748d8add2 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -77,8 +77,7 @@ let functional_induction with_clean c princl pat = user_err (str "Cannot find induction principle for " ++ Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') ) in - let princ = EConstr.of_constr princ in - (princ,NoBindings,Tacmach.pf_unsafe_type_of g' princ,g') + (princ,NoBindings,Tacmach.pf_unsafe_type_of g' princ,g') | _ -> raise (UserError(None,str "functional induction must be used with a function" )) end | Some ((princ,binding)) -> @@ -261,7 +260,6 @@ let derive_inversion fix_names = let evd,c = Evd.fresh_global (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident id)) in - let c = EConstr.of_constr c in let (cst, u) = destConst evd c in evd, (cst, EInstance.kind evd u) :: l ) @@ -283,8 +281,7 @@ let derive_inversion fix_names = (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident (mk_rel_id id))) in - let id = EConstr.of_constr id in - evd,(fst (destInd evd id))::l + evd,(fst (destInd evd id))::l ) fix_names (evd',[]) @@ -388,7 +385,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error let evd = ref (Evd.from_env env) in let evd',uprinc = Evd.fresh_global env !evd princ in let _ = evd := evd' in - let princ_type = Typing.e_type_of ~refresh:true env evd (EConstr.of_constr uprinc) in + let princ_type = Typing.e_type_of ~refresh:true env evd uprinc in let princ_type = EConstr.Unsafe.to_constr princ_type in Functional_principles_types.generate_functional_principle evd @@ -425,7 +422,6 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp let evd,c = Evd.fresh_global (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in - let c = EConstr.of_constr c in let (cst, u) = destConst evd c in let u = EInstance.kind evd u in evd,((cst, u) :: l) @@ -442,7 +438,6 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp let evd,c = Evd.fresh_global (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in - let c = EConstr.of_constr c in let (cst, u) = destConst evd c in let u = EInstance.kind evd u in evd,((cst, u) :: l) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index ae84eaa93..28e85268a 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -102,7 +102,6 @@ let generate_type evd g_to_f f graph i = let evd',graph = Evd.fresh_global (Global.env ()) !evd (Globnames.IndRef (fst (destInd !evd graph))) in - let graph = EConstr.of_constr graph in evd:=evd'; let graph_arity = Typing.e_type_of (Global.env ()) evd graph in let ctxt,_ = decompose_prod_assum !evd graph_arity in @@ -172,7 +171,6 @@ let find_induction_principle evd f = | None -> raise Not_found | Some rect_lemma -> let evd',rect_lemma = Evd.fresh_global (Global.env ()) !evd (Globnames.ConstRef rect_lemma) in - let rect_lemma = EConstr.of_constr rect_lemma in let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in evd:=evd'; rect_lemma,typ @@ -823,8 +821,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list (* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *) let _,lem_cst_constr = Evd.fresh_global (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in - let lem_cst_constr = EConstr.of_constr lem_cst_constr in - let (lem_cst,_) = destConst !evd lem_cst_constr in + let (lem_cst,_) = destConst !evd lem_cst_constr in update_Function {finfo with correctness_lemma = Some lem_cst}; ) @@ -884,8 +881,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let finfo = find_Function_infos (fst f_as_constant) in let _,lem_cst_constr = Evd.fresh_global (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in - let lem_cst_constr = EConstr.of_constr lem_cst_constr in - let (lem_cst,_) = destConst !evd lem_cst_constr in + let (lem_cst,_) = destConst !evd lem_cst_constr in update_Function {finfo with completeness_lemma = Some lem_cst} ) funs) diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 2e90ce90c..a5f8060ae 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -296,7 +296,6 @@ let project_hint ~poly pri l2r r = let env = Global.env() in let sigma = Evd.from_env env in let sigma, c = Evd.fresh_global env sigma gr in - let c = EConstr.of_constr c in let t = Retyping.get_type_of env sigma c in let t = Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) t in @@ -307,7 +306,6 @@ let project_hint ~poly pri l2r r = let p = if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in let sigma, p = Evd.fresh_global env sigma p in - let p = EConstr.of_constr p in let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in let c = it_mkLambda_or_LetIn (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index d32a2faef..9eb55aa5e 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -428,7 +428,8 @@ let split_head = function | [] -> assert(false) let eq_pb (ty, env, x, y as pb) (ty', env', x', y' as pb') = - pb == pb' || (ty == ty' && Constr.equal x x' && Constr.equal y y') + let equal x y = Constr.equal (EConstr.Unsafe.to_constr x) (EConstr.Unsafe.to_constr y) in + pb == pb' || (ty == ty' && equal x x' && equal y y') let problem_inclusion x y = List.for_all (fun pb -> List.exists (fun pb' -> eq_pb pb pb') y) x @@ -626,9 +627,9 @@ let solve_remaining_by env sigma holes by = (** Evar should not be defined, but just in case *) | Some evi -> let env = Environ.reset_with_named_context evi.evar_hyps env in - let ty = EConstr.of_constr evi.evar_concl in + let ty = evi.evar_concl in let c, sigma = Pfedit.refine_by_tactic env sigma ty solve_tac in - Evd.define evk c sigma + Evd.define evk (EConstr.of_constr c) sigma in List.fold_left solve sigma indep @@ -1862,7 +1863,6 @@ let declare_projection n instance_id r = let env = Global.env () in let sigma = Evd.from_env env in let sigma,c = Evd.fresh_global env sigma r in - let c = EConstr.of_constr c in let ty = Retyping.get_type_of env sigma c in let term = proper_projection sigma c ty in let sigma, typ = Typing.type_of env sigma term in diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index e07bc48a4..06c26edbe 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -509,11 +509,12 @@ let pf_abs_evars2 gl rigid (sigma, c0) = let nenv = env_size (pf_env gl) in let abs_evar n k = let evi = Evd.find sigma k in - let dc = CList.firstn n (evar_filtered_context evi) in + let concl = EConstr.Unsafe.to_constr evi.evar_concl in + let dc = EConstr.Unsafe.to_named_context (CList.firstn n (evar_filtered_context evi)) in let abs_dc c = function | NamedDecl.LocalDef (x,b,t) -> mkNamedLetIn x b t (mkArrow t c) | NamedDecl.LocalAssum (x,t) -> mkNamedProd x t c in - let t = Context.Named.fold_inside abs_dc ~init:evi.evar_concl dc in + let t = Context.Named.fold_inside abs_dc ~init:concl dc in nf_evar sigma t in let rec put evlist c = match Constr.kind c with | Evar (k, a) -> @@ -569,11 +570,12 @@ let pf_abs_evars_pirrel gl (sigma, c0) = let nenv = env_size (pf_env gl) in let abs_evar n k = let evi = Evd.find sigma k in - let dc = CList.firstn n (evar_filtered_context evi) in + let concl = EConstr.Unsafe.to_constr evi.evar_concl in + let dc = EConstr.Unsafe.to_named_context (CList.firstn n (evar_filtered_context evi)) in let abs_dc c = function | NamedDecl.LocalDef (x,b,t) -> mkNamedLetIn x b t (mkArrow t c) | NamedDecl.LocalAssum (x,t) -> mkNamedProd x t c in - let t = Context.Named.fold_inside abs_dc ~init:evi.evar_concl dc in + let t = Context.Named.fold_inside abs_dc ~init:concl dc in nf_evar sigma0 (nf_evar sigma t) in let rec put evlist c = match Constr.kind c with | Evar (k, a) -> @@ -581,7 +583,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) = let n = max 0 (Array.length a - nenv) in let k_ty = Retyping.get_sort_family_of - (pf_env gl) sigma (EConstr.of_constr (Evd.evar_concl (Evd.find sigma k))) in + (pf_env gl) sigma (Evd.evar_concl (Evd.find sigma k)) in let is_prop = k_ty = InProp in let t = abs_evar n k in (k, (n, t, is_prop)) :: put evlist t | _ -> Constr.fold put evlist c in @@ -746,7 +748,7 @@ let pf_mkSsrConst name gl = let pf_fresh_global name gl = let sigma, env, it = project gl, pf_env gl, sig_it gl in let sigma,t = Evd.fresh_global env sigma name in - t, re_sig it sigma + EConstr.Unsafe.to_constr t, re_sig it sigma let mkProt t c gl = let prot, gl = pf_mkSsrConst "protect_term" gl in @@ -980,7 +982,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl = if not (EConstr.Vars.closed0 sigma ty) then raise dependent_apply_error; let m = Evarutil.new_meta () in - loop (meta_declare m (EConstr.Unsafe.to_constr ty) sigma) bo ((EConstr.mkMeta m)::args) (n-1) + loop (meta_declare m ty sigma) bo ((EConstr.mkMeta m)::args) (n-1) | _ -> assert false in loop sigma t [] n in pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t)); diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 717657a24..de8ffb976 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -356,7 +356,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac let ev = List.fold_left Evar.Set.union Evar.Set.empty patterns_ev in let ty_ev = Evar.Set.fold (fun i e -> let ex = i in - let i_ty = EConstr.of_constr (Evd.evar_concl (Evd.find (project gl) ex)) in + let i_ty = Evd.evar_concl (Evd.find (project gl) ex) in Evar.Set.union e (evars_of_term i_ty)) ev Evar.Set.empty in let inter = Evar.Set.inter ev ty_ev in diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 2f0433b64..7748ba2b0 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -359,7 +359,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = let evs = Evar.Set.elements (Evarutil.undefined_evars_of_term sigma t) in let open_evs = List.filter (fun k -> Sorts.InProp <> Retyping.get_sort_family_of - env sigma (EConstr.of_constr (Evd.evar_concl (Evd.find sigma k)))) + env sigma (Evd.evar_concl (Evd.find sigma k))) evs in if open_evs <> [] then Some name else None) (List.combine (Array.to_list args) names) @@ -478,10 +478,10 @@ let rwprocess_rule dir rule gl = | _ -> let ra = Array.append a [|r|] in function 1 -> let sigma, pi1 = Evd.fresh_global env sigma coq_prod.Coqlib.proj1 in - EConstr.mkApp (EConstr.of_constr pi1, ra), sigma + EConstr.mkApp (pi1, ra), sigma | _ -> let sigma, pi2 = Evd.fresh_global env sigma coq_prod.Coqlib.proj2 in - EConstr.mkApp (EConstr.of_constr pi2, ra), sigma in + EConstr.mkApp (pi2, ra), sigma in if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_True ())) then let s, sigma = sr sigma 2 in loop (converse_dir d) sigma s a.(1) rs 0 diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index af78bf36a..6b7a96deb 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -623,7 +623,7 @@ let tacFIND_ABSTRACT_PROOF check_lock abstract_n = Goal.enter_one ~__LOC__ begin fun g -> let sigma, env = Goal.(sigma g, env g) in let l = Evd.fold_undefined (fun e ei l -> - match EConstr.kind sigma (EConstr.of_constr ei.Evd.evar_concl) with + match EConstr.kind sigma ei.Evd.evar_concl with | Term.App(hd, [|ty; n; lock|]) when (not check_lock || (occur_existential_or_casted_meta sigma ty && diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index afe03533d..fc50b24a6 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -265,7 +265,7 @@ Goal.enter_one ~__LOC__ begin fun g -> List.fold_left (fun l k -> if Evd.is_defined sigma k then let bo = get_body Evd.(evar_body (find sigma k)) in - k :: l @ Evar.Set.elements (evars_of_econstr sigma bo) + k :: l @ Evar.Set.elements (evars_of_econstr sigma (EConstr.Unsafe.to_constr bo)) else l ) [] s in let und0 = (* Unassigned evars in the initial goal *) diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 2ba6acc03..a10437a63 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -283,7 +283,7 @@ exception NoProgress (* comparison can be much faster than the HO one. *) let unif_EQ env sigma p c = - let evars = existential_opt_value sigma, Evd.universes sigma in + let evars = existential_opt_value0 sigma, Evd.universes sigma in try let _ = Reduction.conv env p ~evars c in true with _ -> false let unif_EQ_args env sigma pa a = @@ -337,7 +337,7 @@ let nf_open_term sigma0 ise c = let s = ise and s' = ref sigma0 in let rec nf c' = match kind c' with | Evar ex -> - begin try nf (existential_value s ex) with _ -> + begin try nf (existential_value0 s ex) with _ -> let k, a = ex in let a' = Array.map nf a in if not (Evd.mem !s' k) then s' := Evd.add !s' k (Evarutil.nf_evar_info s (Evd.find s k)); @@ -347,7 +347,9 @@ let nf_open_term sigma0 ise c = let copy_def k evi () = if evar_body evi != Evd.Evar_empty then () else match Evd.evar_body (Evd.find s k) with - | Evar_defined c' -> s' := Evd.define k (nf c') !s' + | Evar_defined c' -> + let c' = EConstr.of_constr (nf (EConstr.Unsafe.to_constr c')) in + s' := Evd.define k c' !s' | _ -> () in let c' = nf c in let _ = Evd.fold copy_def sigma0 () in !s', Evd.evar_universe_context s, EConstr.of_constr c' @@ -446,7 +448,7 @@ let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 = let nenv = env_size env + if hack then 1 else 0 in let rec put c = match kind c with | Evar (k, a as ex) -> - begin try put (existential_value !sigma ex) + begin try put (existential_value0 !sigma ex) with NotInstantiatedEvar -> if Evd.mem sigma0 k then map put c else let evi = Evd.find !sigma k in @@ -457,11 +459,13 @@ let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 = | Context.Named.Declaration.LocalAssum (x, t) -> mkVar x :: d, mkNamedProd x (put t) c in let a, t = - Context.Named.fold_inside abs_dc ~init:([], (put evi.evar_concl)) dc in + Context.Named.fold_inside abs_dc + ~init:([], (put @@ EConstr.Unsafe.to_constr evi.evar_concl)) + (EConstr.Unsafe.to_named_context dc) in let m = Evarutil.new_meta () in - ise := meta_declare m t !ise; - sigma := Evd.define k (applistc (mkMeta m) a) !sigma; - put (existential_value !sigma ex) + ise := meta_declare m (EConstr.of_constr t) !ise; + sigma := Evd.define k (EConstr.of_constr (applistc (mkMeta m) a)) !sigma; + put (existential_value0 !sigma ex) end | _ -> map put c in let c1 = put c0 in !ise, c1 @@ -541,7 +545,7 @@ let splay_app ise = | App (f, a') -> loop f (Array.append a' a) | Cast (c', _, _) -> loop c' a | Evar ex -> - (try loop (existential_value ise ex) a with _ -> c, a) + (try loop (existential_value0 ise ex) a with _ -> c, a) | _ -> c, a in fun c -> match kind c with | App (f, a) -> loop f a @@ -1255,7 +1259,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let fs sigma x = nf_evar sigma x in let pop_evar sigma e p = let { Evd.evar_body = e_body } as e_def = Evd.find sigma e in - let e_body = match e_body with Evar_defined c -> c + let e_body = match e_body with Evar_defined c -> EConstr.Unsafe.to_constr c | _ -> errorstrm (str "Matching the pattern " ++ pr_constr_env env0 sigma0 p ++ str " did not instantiate ?" ++ int (Evar.repr e) ++ spc () ++ str "Does the variable bound by the \"in\" construct occur "++ -- cgit v1.2.3