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.

6 files changed, 9 insertions, 26 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 0c0d9bcfc..15a24fb37 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -8,8 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-module CVars = Vars
-
 open Pp
 open Util
 open Names
@@ -82,14 +80,13 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl =
     if poly then
       (** Refresh the instance of the hint *)
       let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in
-      let map c = CVars.subst_univs_level_constr subst c in
       let emap c = Vars.subst_univs_level_constr subst c in
       let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
       (** Only metas are mentioning the old universes. *)
       let clenv = {
         templval = Evd.map_fl emap clenv.templval;
         templtyp = Evd.map_fl emap clenv.templtyp;
-        evd = Evd.map_metas map evd;
+        evd = Evd.map_metas emap evd;
         env = Proofview.Goal.env gl;
       } in
       clenv, emap c
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 0260460e6..b11e36bce 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1030,8 +1030,8 @@ module Intpart = Unionfind.Make(Evar.Set)(Evar.Map)
 
 let deps_of_constraints cstrs evm p =
   List.iter (fun (_, _, x, y) ->
-    let evx = Evarutil.undefined_evars_of_term evm (EConstr.of_constr x) in
-    let evy = Evarutil.undefined_evars_of_term evm (EConstr.of_constr y) in
+    let evx = Evarutil.undefined_evars_of_term evm x in
+    let evy = Evarutil.undefined_evars_of_term evm y in
     Intpart.union_set (Evar.Set.union evx evy) p)
     cstrs
 
@@ -1076,7 +1076,7 @@ let error_unresolvable env comp evd =
   | Some s -> Evar.Set.mem ev s
   in
   let fold ev evi (found, accu) =
-    let ev_class = class_of_constr evd (EConstr.of_constr evi.evar_concl) in
+    let ev_class = class_of_constr evd evi.evar_concl in
     if not (Option.is_empty ev_class) && is_part ev then
       (* focus on one instance if only one was searched for *)
       if not found then (true, Some ev)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 98f627f21..d7a3e9470 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1108,8 +1108,6 @@ let make_tuple env sigma (rterm,rty) lind =
   let p = mkLambda (na, a, rty) in
   let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in
   let sigma, sig_term = Evd.fresh_global env sigma sigdata.typ in
-  let exist_term = EConstr.of_constr exist_term in
-  let sig_term = EConstr.of_constr sig_term in
     sigma,
     (applist(exist_term,[a;p;(mkRel lind);rterm]),
      applist(sig_term,[a;p]))
@@ -1203,7 +1201,6 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
             let w_type = unsafe_type_of env !evdref w in
             if Evarconv.e_cumul env evdref w_type a then
 	      let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in
-	      let exist_term = EConstr.of_constr exist_term in
               applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
             else
               user_err Pp.(str "Cannot solve a unification problem.")
@@ -1372,7 +1369,6 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
       let sigma, (injbody,resty) = build_injector e_env !evdref t1' (mkVar e) cpath in
       let injfun = mkNamedLambda e t injbody in
       let sigma,congr = Evd.fresh_global env sigma eq.congr in
-      let congr = EConstr.of_constr congr in
       let pf = applist(congr,[t;resty;injfun;t1;t2]) in
       let sigma, pf_typ = Typing.type_of env sigma pf in
       let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
diff --git a/tactics/inv.ml b/tactics/inv.ml
index d76c9a697..412954989 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -124,12 +124,10 @@ let make_inv_predicate env evd indf realargs id status concl =
 	in
         let eq_term = eqdata.Coqlib.eq in
 	let eq = Evarutil.evd_comb1 (Evd.fresh_global env) evd eq_term in
-        let eq = EConstr.of_constr eq in
         let eqn = applist (eq,[eqnty;lhs;rhs]) in
         let eqns = (Anonymous, lift n eqn) :: eqns in
         let refl_term = eqdata.Coqlib.refl in
 	let refl_term = Evarutil.evd_comb1 (Evd.fresh_global env) evd refl_term in
-	let refl_term = EConstr.of_constr refl_term in
         let refl = mkApp (refl_term, [|eqnty; rhs|]) in
 	let _ = Evarutil.evd_comb1 (Typing.type_of env) evd refl in
         let args = refl :: args in
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index a97ae8f65..5e81e2d4b 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -263,7 +263,7 @@ let pf_with_evars glsev k gls =
     tclTHEN (Refiner.tclEVARS evd) (k a) gls
 
 let pf_constr_of_global gr k =
-  pf_with_evars (fun gls -> on_snd EConstr.of_constr (pf_apply Evd.fresh_global gls gr)) k
+  pf_with_evars (fun gls -> pf_apply Evd.fresh_global gls gr) k
 
 (** Tacticals of Ltac defined directly in term of Proofview *)
 module New = struct
@@ -506,7 +506,7 @@ module New = struct
       let evi = Evd.find sigma evk in
       match Evd.evar_body evi with
       | Evd.Evar_empty -> Some (evk,evi)
-      | Evd.Evar_defined c -> match Constr.kind c with
+      | Evd.Evar_defined c -> match Constr.kind (EConstr.Unsafe.to_constr c) with
         | Term.Evar (evk,l) -> is_undefined_up_to_restriction sigma evk
         | _ -> 
           (* We make the assumption that there is no way to refine an
@@ -709,7 +709,7 @@ module New = struct
   let gl_make_elim ind = begin fun gl ->
     let gr = Indrec.lookup_eliminator (fst ind) (elimination_sort_of_goal gl) in
     let (sigma, c) = pf_apply Evd.fresh_global gl gr in
-    (sigma, EConstr.of_constr c)
+    (sigma, c)
   end
 
   let gl_make_case_dep (ind, u) = begin fun gl ->
@@ -769,7 +769,6 @@ module New = struct
     Proofview.tclEVARMAP >>= fun sigma ->
     Proofview.tclENV >>= fun env ->
     let (sigma, c) = Evd.fresh_global env sigma ref in
-    let c = EConstr.of_constr c in
     Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT c
 
 end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d0ec3358a..efb46e7d9 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1258,7 +1258,6 @@ let cut c =
   end
 
 let error_uninstantiated_metas t clenv =
-  let t = EConstr.Unsafe.to_constr t in
   let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in
   let id = match na with Name id -> id | _ -> anomaly (Pp.str "unnamed dependent meta.")
   in user_err  (str "Cannot find an instance for " ++ Id.print id ++ str".")
@@ -1268,7 +1267,7 @@ let check_unresolved_evars_of_metas sigma clenv =
   (* Refiner.pose_all_metas_as_evars are resolved *)
   List.iter (fun (mv,b) -> match b with
   | Clval (_,(c,_),_) ->
-    (match Constr.kind c.rebus with
+    (match Constr.kind (EConstr.Unsafe.to_constr c.rebus) with
     | Evar (evk,_) when Evd.is_undefined clenv.evd evk
                      && not (Evd.mem sigma evk) ->
       error_uninstantiated_metas (mkMeta mv) clenv
@@ -1445,9 +1444,7 @@ let is_nonrec mind = (Global.lookup_mind (fst mind)).mind_finite == Declarations
 
 let find_ind_eliminator ind s gl =
   let gr = lookup_eliminator ind s in
-  let evd, c = Tacmach.New.pf_apply Evd.fresh_global gl gr in
-  let c = EConstr.of_constr c in
-    evd, c
+  Tacmach.New.pf_apply Evd.fresh_global gl gr
 
 let find_eliminator c gl =
   let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_unsafe_type_of gl c) in
@@ -2612,9 +2609,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
           let eqdata = build_coq_eq_data () in
           let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in
           let (sigma, eq) = Evd.fresh_global env sigma eqdata.eq in
-          let eq = EConstr.of_constr eq in
           let (sigma, refl) = Evd.fresh_global env sigma eqdata.refl in
-          let refl = EConstr.of_constr refl in
           let eq = applist (eq,args) in
           let refl = applist (refl, [t;mkVar id]) in
 	  let term = mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)) in
@@ -2668,9 +2663,7 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
       let eqdata = build_coq_eq_data () in
       let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in
       let (sigma, eq) = Evd.fresh_global env sigma eqdata.eq in
-      let eq = EConstr.of_constr eq in
       let (sigma, refl) = Evd.fresh_global env sigma eqdata.refl in
-      let refl = EConstr.of_constr refl in
       let eq = applist (eq,args) in
       let refl = applist (refl, [t;mkVar id]) in
       let newenv = insert_before [LocalAssum (heq,eq); decl] lastlhyp env in