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.

5 files changed, 15 insertions, 13 deletions

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 *)