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.

14 files changed, 53 insertions, 55 deletions

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 "++