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.

8 files changed, 258 insertions, 212 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 01b4fe851..a72bdee12 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -13,138 +13,8 @@ open Util
 open Names
 open Constr
 open Context
-open Evd
-
-module API :
-sig
-module ESorts :
-sig
-type t
-val make : Sorts.t -> t
-val kind : Evd.evar_map -> t -> Sorts.t
-val unsafe_to_sorts : t -> Sorts.t
-end
-module EInstance :
-sig
-type t
-val make : Univ.Instance.t -> t
-val kind : Evd.evar_map -> t -> Univ.Instance.t
-val empty : t
-val is_empty : t -> bool
-val unsafe_to_instance : t -> Univ.Instance.t
-end
-type t
-val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term
-val kind_upto : Evd.evar_map -> constr -> (constr, types, Sorts.t, Univ.Instance.t) Constr.kind_of_term
-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 : ?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
-val unsafe_to_named_decl : (t, t) Context.Named.Declaration.pt -> (Constr.t, Constr.types) Context.Named.Declaration.pt
-val unsafe_to_rel_decl : (t, t) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt
-val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, t) Context.Rel.Declaration.pt
-val to_rel_decl : Evd.evar_map -> (t, t) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt
-end =
-struct
-
-module ESorts =
-struct
-  type t = Sorts.t
-  let make s = s
-  let kind sigma = function
-  | Sorts.Type u -> Sorts.sort_of_univ (Evd.normalize_universe sigma u)
-  | s -> s
-  let unsafe_to_sorts s = s
-end
 
-module EInstance =
-struct
-  type t = Univ.Instance.t
-  let make i = i
-  let kind sigma i =
-    if Univ.Instance.is_empty i then i
-    else Evd.normalize_universe_instance sigma i
-  let empty = Univ.Instance.empty
-  let is_empty = Univ.Instance.is_empty
-  let unsafe_to_instance t = t
-end
-
-type t = Constr.t
-
-let safe_evar_value sigma ev =
-  try Some (Evd.existential_value sigma ev)
-  with NotInstantiatedEvar | Not_found -> None
-
-let rec whd_evar sigma c =
-  match Constr.kind c with
-  | Evar ev ->
-    begin match safe_evar_value sigma ev with
-    | Some c -> whd_evar sigma c
-    | None -> c
-    end
-  | App (f, args) when isEvar f ->
-    (** Enforce smart constructor invariant on applications *)
-    let ev = destEvar f in
-    begin match safe_evar_value sigma ev with
-    | None -> c
-    | Some f -> whd_evar sigma (mkApp (f, args))
-    end
-  | Cast (c0, k, t) when isEvar c0 ->
-    (** Enforce smart constructor invariant on casts. *)
-    let ev = destEvar c0 in
-    begin match safe_evar_value sigma ev with
-    | None -> c
-    | Some c -> whd_evar sigma (mkCast (c, k, t))
-    end
-  | _ -> c
-
-let kind sigma c = Constr.kind (whd_evar sigma c)
-let kind_upto = kind
-let kind_of_type sigma c = Term.kind_of_type (whd_evar sigma c)
-let of_kind = Constr.of_kind
-let of_constr c = c
-let unsafe_to_constr c = c
-let unsafe_eq = Refl
-
-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 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
-  if u' == u then c else mkSort (Sorts.sort_of_univ u')
-| Const (c', u) when not (Univ.Instance.is_empty u) ->
-  let u' = Evd.normalize_universe_instance sigma u in
-  if u' == u then c else mkConstU (c', u')
-| Ind (i, u) when not (Univ.Instance.is_empty u) ->
-  let u' = Evd.normalize_universe_instance sigma u in
-  if u' == u then c else mkIndU (i, u')
-| 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 c) c
-in to_constr c
-
-let of_named_decl d = d
-let unsafe_to_named_decl d = d
-let of_rel_decl d = d
-let unsafe_to_rel_decl d = d
-let to_rel_decl sigma d = Context.Rel.Declaration.map_constr (to_constr sigma) d
-
-end
-
-include API
+include Evd.MiniEConstr
 
 type types = t
 type constr = t
@@ -387,8 +257,7 @@ let decompose_prod_n_assum sigma n c =
   in
   prodec_rec Context.Rel.empty n c
 
-let existential_type sigma (evk, args) =
-  of_constr (existential_type sigma (evk, Array.map unsafe_to_constr args))
+let existential_type = Evd.existential_type
 
 let map sigma f c = match kind sigma c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
@@ -749,7 +618,7 @@ let universes_of_constr env sigma c =
          LSet.fold LSet.add (Universe.levels u) s
     | Evar (k, args) ->
        let concl = Evd.evar_concl (Evd.find sigma k) in
-       fold sigma aux (aux s (of_constr concl)) c
+       fold sigma aux (aux s concl) c
     | _ -> fold sigma aux s c
   in aux LSet.empty c
 
@@ -907,6 +776,10 @@ let named_context e = cast_named_context (sym unsafe_eq) (named_context e)
 let val_of_named_context e = val_of_named_context (cast_named_context unsafe_eq e)
 let named_context_of_val e = cast_named_context (sym unsafe_eq) (named_context_of_val e)
 
+let of_existential : Constr.existential -> existential =
+  let gen : type a b. (a,b) eq -> 'c * b array -> 'c * a array = fun Refl x -> x in
+  gen unsafe_eq
+
 let lookup_rel i e = cast_rel_decl (sym unsafe_eq) (lookup_rel i e)
 let lookup_named n e = cast_named_decl (sym unsafe_eq) (lookup_named n e)
 let lookup_named_val n e = cast_named_decl (sym unsafe_eq) (lookup_named_val n e)
@@ -922,7 +795,7 @@ let map_rel_context_in_env f env sign =
 
 let fresh_global ?loc ?rigid ?names env sigma reference =
   let (evd,t) = Evd.fresh_global ?loc ?rigid ?names env sigma reference in
-  evd, of_constr t
+  evd, t
 
 let is_global sigma gr c =
   Globnames.is_global gr (to_constr sigma c)
@@ -934,5 +807,10 @@ let to_instance = EInstance.unsafe_to_instance
 let to_constr = unsafe_to_constr
 let to_rel_decl = unsafe_to_rel_decl
 let to_named_decl = unsafe_to_named_decl
+let to_named_context =
+  let gen : type a b. (a, b) eq -> (a,a) Context.Named.pt -> (b,b) Context.Named.pt
+    = fun Refl x -> x
+  in
+  gen unsafe_eq
 let eq = unsafe_eq
 end
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 9cc9bf680..9a5b5ec3a 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -13,7 +13,7 @@ open Names
 open Constr
 open Environ
 
-type t
+type t = Evd.econstr
 (** Type of incomplete terms. Essentially a wrapper around {!Constr.t} ensuring
     that {!Constr.kind} does not observe defined evars. *)
 
@@ -290,6 +290,7 @@ val is_global : Evd.evar_map -> Globnames.global_reference -> t -> bool
 
 (** {5 Extra} *)
 
+val of_existential : Constr.existential -> existential
 val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, types) Context.Named.Declaration.pt
 val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, types) Context.Rel.Declaration.pt
 
@@ -308,6 +309,8 @@ sig
   val to_named_decl : (t, types) Context.Named.Declaration.pt -> (Constr.t, Constr.types) Context.Named.Declaration.pt
   (** Physical identity. Does not care for defined evars. *)
 
+  val to_named_context : (t, types) Context.Named.pt -> Context.Named.t
+
   val to_sorts : ESorts.t -> Sorts.t
   (** Physical identity. Does not care for normalization. *)
 
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index c707b37b6..065b42bf6 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -23,7 +23,8 @@ module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
 let safe_evar_value sigma ev =
-  try Some (Evd.existential_value sigma ev)
+  let ev = EConstr.of_existential ev in
+  try Some (EConstr.Unsafe.to_constr @@ Evd.existential_value sigma ev)
   with NotInstantiatedEvar | Not_found -> None
 
 (** Combinators *)
@@ -44,11 +45,11 @@ let evd_comb2 f evdref x y =
     z
 
 let e_new_global evdref x = 
-  EConstr.of_constr (evd_comb1 (Evd.fresh_global (Global.env())) evdref x)
+  evd_comb1 (Evd.fresh_global (Global.env())) evdref x
 
 let new_global evd x = 
   let (evd, c) = Evd.fresh_global (Global.env()) evd x in
-  (evd, EConstr.of_constr c)
+  (evd, c)
 
 (****************************************************)
 (* Expanding/testing/exposing existential variables *)
@@ -61,7 +62,7 @@ exception Uninstantiated_evar of Evar.t
 let rec flush_and_check_evars sigma c =
   match kind c with
   | Evar (evk,_ as ev) ->
-      (match existential_opt_value sigma ev with
+      (match existential_opt_value0 sigma ev with
        | None -> raise (Uninstantiated_evar evk)
        | Some c -> flush_and_check_evars sigma c)
   | _ -> Constr.map (flush_and_check_evars sigma) c
@@ -102,7 +103,8 @@ let nf_evar_map_universes evm =
     if Univ.LMap.is_empty subst then evm, nf_evar0 evm
     else
       let f = nf_evars_universes evm in
-	Evd.raw_map (fun _ -> map_evar_info f) evm, f
+      let f' c = EConstr.of_constr (f (EConstr.Unsafe.to_constr c)) in
+        Evd.raw_map (fun _ -> map_evar_info f') evm, f
 
 let nf_named_context_evar sigma ctx =
   Context.Named.map (nf_evar0 sigma) ctx
@@ -115,7 +117,7 @@ let nf_env_evar sigma env =
   let rel' = nf_rel_context_evar sigma (EConstr.rel_context env) in
     EConstr.push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env)
 
-let nf_evar_info evc info = map_evar_info (nf_evar0 evc) info
+let nf_evar_info evc info = map_evar_info (nf_evar evc) info
 
 let nf_evar_map evm =
   Evd.raw_map (fun _ evi -> nf_evar_info evm evi) evm
@@ -414,7 +416,6 @@ let push_rel_context_to_named_context env sigma typ =
 let default_source = Loc.tag @@ Evar_kinds.InternalHole
 
 let restrict_evar evd evk filter ?src candidates =
-  let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in
   let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in
   Evd.declare_future_goal evk' evd, evk'
 
@@ -424,8 +425,6 @@ let new_pure_evar_full evd evi =
   (evd, evk)
 
 let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ =
-  let typ = EConstr.Unsafe.to_constr typ in
-  let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in
   let default_naming = Misctypes.IntroAnonymous in
   let naming = Option.default default_naming naming in
   let name = match naming with
@@ -513,7 +512,7 @@ let generalize_evar_over_rels sigma (ev,args) =
   List.fold_left2
     (fun (c,inst as x) a d ->
       if isRel sigma a then (mkNamedProd_or_LetIn d c,a::inst) else x)
-     (EConstr.of_constr evi.evar_concl,[]) (Array.to_list args) sign
+     (evi.evar_concl,[]) (Array.to_list args) sign
 
 (************************************)
 (* Removing a dependency in an evar *)
@@ -549,7 +548,8 @@ let rec check_and_clear_in_constr env evdref err ids global c =
       | Evar (evk,l as ev) ->
 	  if Evd.is_defined !evdref evk then
 	    (* If evk is already defined we replace it by its definition *)
-	    let nc = Evd.existential_value !evdref ev in
+            let nc = Evd.existential_value !evdref (EConstr.of_existential ev) in
+            let nc = EConstr.Unsafe.to_constr nc in
 	      (check_and_clear_in_constr env evdref err ids global nc)
 	  else
 	    (* We check for dependencies to elements of ids in the
@@ -559,8 +559,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
 	       removed *)
 	    let evi = Evd.find_undefined !evdref evk in
 	    let ctxt = Evd.evar_filtered_context evi in
-	    let ctxt = List.map (fun d -> map_named_decl EConstr.of_constr d) ctxt in
-	    let (rids,filter) =
+            let (rids,filter) =
               List.fold_right2
                 (fun h a (ri,filter) ->
                   try
@@ -586,7 +585,8 @@ let rec check_and_clear_in_constr env evdref err ids global c =
 	      try
                 let nids = Id.Map.domain rids in
                 let global = Id.Set.exists is_section_variable nids in
-                check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids global (evar_concl evi)
+                let concl = EConstr.Unsafe.to_constr (evar_concl evi) in
+                check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids global concl
 	      with ClearDependencyError (rid,err) ->
 		raise (ClearDependencyError (Id.Map.find rid rids,err)) in
 
@@ -597,7 +597,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
               let evd = !evdref in
               let (evd,_) = restrict_evar evd evk filter None in
               evdref := evd;
-              Evd.existential_value !evdref ev
+              Evd.existential_value0 !evdref ev
 
       | _ -> Constr.map (check_and_clear_in_constr env evdref err ids global) c
 
@@ -643,7 +643,7 @@ let clear_hyps2_in_evi env evdref hyps t concl ids =
 let queue_set q is_dependent set =
   Evar.Set.iter (fun a -> Queue.push (is_dependent,a) q) set
 let queue_term q is_dependent c =
-  queue_set q is_dependent (evars_of_term c)
+  queue_set q is_dependent (evars_of_term (EConstr.Unsafe.to_constr c))
 
 let process_dependent_evar q acc evm is_dependent e =
   let evi = Evd.find evm e in
@@ -656,12 +656,12 @@ let process_dependent_evar q acc evm is_dependent e =
     match decl with
     | LocalAssum _ -> ()
     | LocalDef (_,b,_) -> queue_term q true b
-  end (Environ.named_context_of_val evi.evar_hyps);
+  end (EConstr.named_context_of_val evi.evar_hyps);
   match evi.evar_body with
   | Evar_empty ->
       if is_dependent then Evar.Map.add e None acc else acc
   | Evar_defined b ->
-      let subevars = evars_of_term b in
+      let subevars = evars_of_term (EConstr.Unsafe.to_constr b) in
       (* evars appearing in the definition of an evar [e] are marked
          as dependent when [e] is dependent itself: if [e] is a
          non-dependent goal, then, unless they are reach from another
@@ -729,11 +729,11 @@ let undefined_evars_of_named_context evd nc =
     ~init:Evar.Set.empty
 
 let undefined_evars_of_evar_info evd evi =
-  Evar.Set.union (undefined_evars_of_term evd (EConstr.of_constr evi.evar_concl))
+  Evar.Set.union (undefined_evars_of_term evd evi.evar_concl)
     (Evar.Set.union
        (match evi.evar_body with
 	 | Evar_empty -> Evar.Set.empty
-	 | Evar_defined b -> undefined_evars_of_term evd (EConstr.of_constr b))
+         | Evar_defined b -> undefined_evars_of_term evd b)
        (undefined_evars_of_named_context evd
 	  (named_context_of_val evi.evar_hyps)))
 
@@ -781,10 +781,11 @@ let filtered_undefined_evars_of_evar_info ?cache sigma evi =
   in
   let accu = match evi.evar_body with
   | Evar_empty -> Evar.Set.empty
-  | Evar_defined b -> evars_of_term b
+  | Evar_defined b -> evars_of_term (EConstr.Unsafe.to_constr b)
   in
-  let accu = Evar.Set.union (undefined_evars_of_term sigma (EConstr.of_constr evi.evar_concl)) accu in
-  evars_of_named_context cache accu (evar_filtered_context evi)
+  let accu = Evar.Set.union (undefined_evars_of_term sigma evi.evar_concl) accu in
+  let ctxt = EConstr.Unsafe.to_named_context (evar_filtered_context evi) in
+  evars_of_named_context cache accu ctxt
 
 (* spiwack: this is a more complete version of
    {!Termops.occur_evar}. The latter does not look recursively into an
@@ -794,7 +795,7 @@ let occur_evar_upto sigma n c =
   let c = EConstr.Unsafe.to_constr c in
   let rec occur_rec c = match kind c with
     | Evar (sp,_) when Evar.equal sp n -> raise Occur
-    | Evar e -> Option.iter occur_rec (existential_opt_value sigma e)
+    | Evar e -> Option.iter occur_rec (existential_opt_value0 sigma e)
     | _ -> Constr.iter occur_rec c
   in
   try occur_rec c; false with Occur -> true
@@ -849,6 +850,8 @@ let compare_constructor_instances evd u u' =
 let eq_constr_univs_test sigma1 sigma2 t u =
   (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *)
   let open Evd in
+  let t = EConstr.Unsafe.to_constr t
+  and u = EConstr.Unsafe.to_constr u in
   let fold cstr sigma =
     try Some (add_universe_constraints sigma cstr)
     with Univ.UniverseInconsistency _ | UniversesDiffer -> None
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 972b0b9e1..40c1ee082 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -201,7 +201,7 @@ val kind_of_term_upto : evar_map -> Constr.constr ->
     universes. The term [t] is interpreted in [sigma1] while [u] is
     interpreted in [sigma2]. The universe constraints in [sigma2] are
     assumed to be an extention of those in [sigma1]. *)
-val eq_constr_univs_test : evar_map -> evar_map -> Constr.constr -> Constr.constr -> bool
+val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool
 
 (** [compare_cumulative_instances cv_pb variance u1 u2 sigma] Returns
    [Inl sigma'] where [sigma'] is [sigma] augmented with universe
diff --git a/engine/evd.ml b/engine/evd.ml
index f6e13e1f4..6dcec2760 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -21,6 +21,9 @@ open Environ
 (* module RelDecl = Context.Rel.Declaration *)
 module NamedDecl = Context.Named.Declaration
 
+type econstr = constr
+type etypes = types
+
 (** Generic filters *)
 module Filter :
 sig
@@ -537,10 +540,14 @@ let existential_value d (n, args) =
   | Evar_empty ->
     raise NotInstantiatedEvar
 
+let existential_value0 = existential_value
+
 let existential_opt_value d ev =
   try Some (existential_value d ev)
   with NotInstantiatedEvar -> None
 
+let existential_opt_value0 = existential_opt_value
+
 let existential_type d (n, args) =
   let info =
     try find d n
@@ -548,6 +555,8 @@ let existential_type d (n, args) =
       anomaly (str "Evar " ++ str (string_of_existential n) ++ str " was not declared.") in
   instantiate_evar_array info info.evar_concl args
 
+let existential_type0 = existential_type
+
 let add_constraints d c =
   { d with universes = UState.add_constraints d.universes c }
 
@@ -1065,6 +1074,7 @@ let meta_ftype evd mv =
     | Clval(_,_,b) -> b
 
 let meta_type evd mv = (meta_ftype evd mv).rebus
+let meta_type0 = meta_type
 
 let meta_declare mv v ?(name=Anonymous) evd =
   let metas = Metamap.add mv (Cltyp(name,mk_freelisted v)) evd.metas in
@@ -1217,3 +1227,98 @@ let normalize_evar_universe_context_variables = UState.normalize_variables
 let abstract_undefined_variables = UState.abstract_undefined_variables
 let normalize_evar_universe_context = UState.minimize
 let nf_constraints = minimize_universes
+
+module MiniEConstr = struct
+
+  module ESorts =
+  struct
+    type t = Sorts.t
+    let make s = s
+    let kind sigma = function
+      | Sorts.Type u -> Sorts.sort_of_univ (normalize_universe sigma u)
+      | s -> s
+    let unsafe_to_sorts s = s
+  end
+
+  module EInstance =
+  struct
+    type t = Univ.Instance.t
+    let make i = i
+    let kind sigma i =
+      if Univ.Instance.is_empty i then i
+      else normalize_universe_instance sigma i
+    let empty = Univ.Instance.empty
+    let is_empty = Univ.Instance.is_empty
+    let unsafe_to_instance t = t
+  end
+
+  type t = econstr
+
+  let safe_evar_value sigma ev =
+    try Some (existential_value sigma ev)
+    with NotInstantiatedEvar | Not_found -> None
+
+  let rec whd_evar sigma c =
+    match Constr.kind c with
+    | Evar ev ->
+      begin match safe_evar_value sigma ev with
+        | Some c -> whd_evar sigma c
+        | None -> c
+      end
+    | App (f, args) when isEvar f ->
+      (** Enforce smart constructor invariant on applications *)
+      let ev = destEvar f in
+      begin match safe_evar_value sigma ev with
+        | None -> c
+        | Some f -> whd_evar sigma (mkApp (f, args))
+      end
+    | Cast (c0, k, t) when isEvar c0 ->
+      (** Enforce smart constructor invariant on casts. *)
+      let ev = destEvar c0 in
+      begin match safe_evar_value sigma ev with
+        | None -> c
+        | Some c -> whd_evar sigma (mkCast (c, k, t))
+      end
+    | _ -> c
+
+  let kind sigma c = Constr.kind (whd_evar sigma c)
+  let kind_upto = kind
+  let kind_of_type sigma c = Term.kind_of_type (whd_evar sigma c)
+  let of_kind = Constr.of_kind
+  let of_constr c = c
+  let unsafe_to_constr c = c
+  let unsafe_eq = Refl
+
+  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 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' = normalize_universe sigma u in
+        if u' == u then c else mkSort (Sorts.sort_of_univ u')
+      | Const (c', u) when not (Univ.Instance.is_empty u) ->
+        let u' = normalize_universe_instance sigma u in
+        if u' == u then c else mkConstU (c', u')
+      | Ind (i, u) when not (Univ.Instance.is_empty u) ->
+        let u' = normalize_universe_instance sigma u in
+        if u' == u then c else mkIndU (i, u')
+      | Construct (co, u) when not (Univ.Instance.is_empty u) ->
+        let u' = normalize_universe_instance sigma u in
+        if u' == u then c else mkConstructU (co, u')
+      | _ -> 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
+  let of_rel_decl d = d
+  let unsafe_to_rel_decl d = d
+  let to_rel_decl sigma d = Context.Rel.Declaration.map_constr (to_constr sigma) d
+
+end
diff --git a/engine/evd.mli b/engine/evd.mli
index 911799c44..5ce16459c 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -28,6 +28,9 @@ open Environ
     It also contains conversion constraints, debugging information and
     information about meta variables. *)
 
+type econstr
+type etypes = econstr
+
 (** {5 Existential variables and unification states} *)
 
 type evar = Evar.t
@@ -86,16 +89,16 @@ end
 
 type evar_body =
   | Evar_empty
-  | Evar_defined of constr
+  | Evar_defined of econstr
 
 
 module Store : Store.S
 (** Datatype used to store additional information in evar maps. *)
 
 type evar_info = {
-  evar_concl : constr;
+  evar_concl : econstr;
   (** Type of the evar. *)
-  evar_hyps : named_context_val;
+  evar_hyps : named_context_val; (** TODO econstr? *)
   (** Context of the evar. *)
   evar_body : evar_body;
   (** Optional content of the evar. *)
@@ -105,16 +108,16 @@ type evar_info = {
       in the solution *)
   evar_source : Evar_kinds.t located;
   (** Information about the evar. *)
-  evar_candidates : constr list option;
+  evar_candidates : econstr list option;
   (** List of possible solutions when known that it is a finite list *)
   evar_extra : Store.t
   (** Extra store, used for clever hacks. *)
 }
 
-val make_evar : named_context_val -> types -> evar_info
-val evar_concl : evar_info -> constr
-val evar_context : evar_info -> Context.Named.t
-val evar_filtered_context : evar_info -> Context.Named.t
+val make_evar : named_context_val -> etypes -> evar_info
+val evar_concl : evar_info -> econstr
+val evar_context : evar_info -> (econstr, etypes) Context.Named.pt
+val evar_filtered_context : evar_info -> (econstr, etypes) Context.Named.pt
 val evar_hyps : evar_info -> named_context_val
 val evar_filtered_hyps : evar_info -> named_context_val
 val evar_body : evar_info -> evar_body
@@ -122,8 +125,8 @@ val evar_filter : evar_info -> Filter.t
 val evar_env :  evar_info -> env
 val evar_filtered_env :  evar_info -> env
 
-val map_evar_body : (constr -> constr) -> evar_body -> evar_body
-val map_evar_info : (constr -> constr) -> evar_info -> evar_info
+val map_evar_body : (econstr -> econstr) -> evar_body -> evar_body
+val map_evar_info : (econstr -> econstr) -> evar_info -> evar_info
 
 (** {6 Unification state} **)
 
@@ -190,7 +193,7 @@ val raw_map_undefined : (Evar.t -> evar_info -> evar_info) -> evar_map -> evar_m
 (** Same as {!raw_map}, but restricted to undefined evars. For efficiency
     reasons. *)
 
-val define : Evar.t-> constr -> evar_map -> evar_map
+val define : Evar.t-> econstr -> evar_map -> evar_map
 (** Set the body of an evar to the given constr. It is expected that:
     {ul
       {- The evar is already present in the evarmap.}
@@ -198,7 +201,7 @@ val define : Evar.t-> constr -> evar_map -> evar_map
       {- All the evars present in the constr should be present in the evar map.}
     } *)
 
-val cmap : (constr -> constr) -> evar_map -> evar_map
+val cmap : (econstr -> econstr) -> evar_map -> evar_map
 (** Map the function on all terms in the evar map. *)
 
 val is_evar : evar_map -> Evar.t-> bool
@@ -222,20 +225,26 @@ val drop_all_defined : evar_map -> evar_map
 
 exception NotInstantiatedEvar
 
-val existential_value : evar_map -> existential -> constr
+val existential_value : evar_map -> econstr pexistential -> econstr
 (** [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has
     no body and [Not_found] if it does not exist in [sigma] *)
 
-val existential_type : evar_map -> existential -> types
+val existential_value0 : evar_map -> existential -> constr
+
+val existential_type : evar_map -> econstr pexistential -> etypes
 
-val existential_opt_value : evar_map -> existential -> constr option
+val existential_type0 : evar_map -> existential -> types
+
+val existential_opt_value : evar_map -> econstr pexistential -> econstr option
 (** Same as {!existential_value} but returns an option instead of raising an
     exception. *)
 
+val existential_opt_value0 : evar_map -> existential -> constr option
+
 val evar_instance_array : (Context.Named.Declaration.t -> 'a -> bool) -> evar_info ->
   'a array -> (Id.t * 'a) list
 
-val instantiate_evar_array : evar_info -> constr -> constr array -> constr
+val instantiate_evar_array : evar_info -> econstr -> econstr array -> econstr
 
 val evars_reset_evd  : ?with_conv_pbs:bool -> ?with_univs:bool -> 
   evar_map ->  evar_map -> evar_map
@@ -243,7 +252,7 @@ val evars_reset_evd  : ?with_conv_pbs:bool -> ?with_univs:bool ->
 
 (** {6 Misc} *)
 
-val restrict : Evar.t-> Filter.t -> ?candidates:constr list ->
+val restrict : Evar.t-> Filter.t -> ?candidates:econstr list ->
   ?src:Evar_kinds.t located -> evar_map -> evar_map * Evar.t
 (** Restrict an undefined evar into a new evar by filtering context and
     possibly limiting the instances to a set of candidates *)
@@ -251,7 +260,7 @@ val restrict : Evar.t-> Filter.t -> ?candidates:constr list ->
 val is_restricted_evar : evar_info -> Evar.t option
 (** Tell if an evar comes from restriction of another evar, and if yes, which *)
 
-val downcast : Evar.t-> types -> evar_map -> evar_map
+val downcast : Evar.t-> etypes -> evar_map -> evar_map
 (** Change the type of an undefined evar to a new type assumed to be a
     subtype of its current type; subtyping must be ensured by caller *)
 
@@ -341,7 +350,7 @@ val shelve_on_future_goals : Evar.t list -> future_goals -> future_goals
     Evar maps also keep track of the universe constraints defined at a given
     point. This section defines the relevant manipulation functions. *)
 
-val whd_sort_variable : evar_map -> constr -> constr
+val whd_sort_variable : evar_map -> econstr -> econstr
 
 exception UniversesDiffer
 
@@ -397,8 +406,8 @@ type 'a freelisted = {
   rebus : 'a;
   freemetas : Metaset.t }
 
-val metavars_of : constr -> Metaset.t
-val mk_freelisted : constr -> constr freelisted
+val metavars_of : econstr -> Metaset.t
+val mk_freelisted : econstr -> econstr freelisted
 val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted
 
 (** Status of an instance found by unification wrt to the meta it solves:
@@ -436,12 +445,12 @@ type instance_status = instance_constraint * instance_typing_status
 (** Clausal environments *)
 
 type clbinding =
-  | Cltyp of Name.t * constr freelisted
-  | Clval of Name.t * (constr freelisted * instance_status) * constr freelisted
+  | Cltyp of Name.t * econstr freelisted
+  | Clval of Name.t * (econstr freelisted * instance_status) * econstr freelisted
 
 (** Unification constraints *)
 type conv_pb = Reduction.conv_pb
-type evar_constraint = conv_pb * env * constr * constr
+type evar_constraint = conv_pb * env * econstr * econstr
 val add_conv_pb : ?tail:bool -> evar_constraint -> evar_map -> evar_map
 
 val extract_changed_conv_pbs : evar_map ->
@@ -457,7 +466,7 @@ val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option
 val evars_of_term : constr -> Evar.Set.t
   (** including evars in instances of evars *)
 
-val evars_of_named_context : Context.Named.t -> Evar.Set.t
+val evars_of_named_context : (econstr, etypes) Context.Named.pt -> Evar.Set.t
 
 val evars_of_filtered_evar_info : evar_info -> Evar.Set.t
 
@@ -465,19 +474,20 @@ val evars_of_filtered_evar_info : evar_info -> Evar.Set.t
 val meta_list : evar_map -> (metavariable * clbinding) list
 val meta_defined : evar_map -> metavariable -> bool
 
-val meta_value     : evar_map -> metavariable -> constr
+val meta_value     : evar_map -> metavariable -> econstr
 (** [meta_fvalue] raises [Not_found] if meta not in map or [Anomaly] if
    meta has no value *)
 
-val meta_fvalue    : evar_map -> metavariable -> constr freelisted * instance_status
-val meta_opt_fvalue : evar_map -> metavariable -> (constr freelisted * instance_status) option
-val meta_type      : evar_map -> metavariable -> types
-val meta_ftype     : evar_map -> metavariable -> types freelisted
+val meta_fvalue    : evar_map -> metavariable -> econstr freelisted * instance_status
+val meta_opt_fvalue : evar_map -> metavariable -> (econstr freelisted * instance_status) option
+val meta_type      : evar_map -> metavariable -> etypes
+val meta_type0 : evar_map -> metavariable -> types
+val meta_ftype     : evar_map -> metavariable -> etypes freelisted
 val meta_name      : evar_map -> metavariable -> Name.t
 val meta_declare   :
-  metavariable -> types -> ?name:Name.t -> evar_map -> evar_map
-val meta_assign    : metavariable -> constr * instance_status -> evar_map -> evar_map
-val meta_reassign  : metavariable -> constr * instance_status -> evar_map -> evar_map
+  metavariable -> etypes -> ?name:Name.t -> evar_map -> evar_map
+val meta_assign    : metavariable -> econstr * instance_status -> evar_map -> evar_map
+val meta_reassign  : metavariable -> econstr * instance_status -> evar_map -> evar_map
 
 val clear_metas : evar_map -> evar_map
 
@@ -485,10 +495,10 @@ val clear_metas : evar_map -> evar_map
 val meta_merge : ?with_univs:bool -> evar_map -> evar_map -> evar_map
 
 val undefined_metas : evar_map -> metavariable list
-val map_metas_fvalue : (constr -> constr) -> evar_map -> evar_map
-val map_metas : (constr -> constr) -> evar_map -> evar_map
+val map_metas_fvalue : (econstr -> econstr) -> evar_map -> evar_map
+val map_metas : (econstr -> econstr) -> evar_map -> evar_map
 
-type metabinding = metavariable * constr * instance_status
+type metabinding = metavariable * econstr * instance_status
 
 val retract_coercible_metas : evar_map -> metabinding list * evar_map
 
@@ -639,13 +649,13 @@ val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> eva
 val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor
 
 val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env ->
-  evar_map -> Globnames.global_reference -> evar_map * constr
+  evar_map -> Globnames.global_reference -> evar_map * econstr
 
 (********************************************************************)
 (* constr with holes and pending resolution of classes, conversion  *)
 (* problems, candidates, etc.                                       *)
 
-type open_constr = evar_map * constr (* Special case when before is empty *)
+type open_constr = evar_map * econstr (* Special case when before is empty *)
 
 (** Partially constructed constrs. *)
 
@@ -665,3 +675,50 @@ val create_evar_defs : evar_map -> evar_map
 
 (** Create an [evar_map] with empty meta map: *)
 
+(** Use this module only to bootstrap EConstr *)
+module MiniEConstr : sig
+  module ESorts : sig
+    type t
+    val make : Sorts.t -> t
+    val kind : evar_map -> t -> Sorts.t
+    val unsafe_to_sorts : t -> Sorts.t
+  end
+
+  module EInstance : sig
+    type t
+    val make : Univ.Instance.t -> t
+    val kind : evar_map -> t -> Univ.Instance.t
+    val empty : t
+    val is_empty : t -> bool
+    val unsafe_to_instance : t -> Univ.Instance.t
+  end
+
+  type t = econstr
+
+  val kind : evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term
+  val kind_upto : evar_map -> constr -> (constr, types, Sorts.t, Univ.Instance.t) Constr.kind_of_term
+  val kind_of_type : evar_map -> t -> (t, t) Term.kind_of_type
+
+  val whd_evar : 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 : ?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
+  val unsafe_to_named_decl : (t, t) Context.Named.Declaration.pt ->
+    (Constr.t, Constr.types) Context.Named.Declaration.pt
+  val unsafe_to_rel_decl : (t, t) Context.Rel.Declaration.pt ->
+    (Constr.t, Constr.types) Context.Rel.Declaration.pt
+  val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt ->
+    (t, t) Context.Rel.Declaration.pt
+  val to_rel_decl : evar_map -> (t, t) Context.Rel.Declaration.pt ->
+    (Constr.t, Constr.types) Context.Rel.Declaration.pt
+end
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 639f48e77..54237ceb4 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -45,9 +45,9 @@ let compact el ({ solution } as pv) =
   let pruned_solution = Evd.drop_all_defined solution in
   let apply_subst_einfo _ ei =
     Evd.({ ei with
-       evar_concl =  nf0 ei.evar_concl;
+       evar_concl =  nf ei.evar_concl;
        evar_hyps = Environ.map_named_val nf0 ei.evar_hyps;
-       evar_candidates = Option.map (List.map nf0) ei.evar_candidates }) in
+       evar_candidates = Option.map (List.map nf) ei.evar_candidates }) in
   let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in
   let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in
   Feedback.msg_info (Pp.str (Printf.sprintf "Evars: %d -> %d\n" size new_size));
@@ -875,8 +875,7 @@ module Progress = struct
 
   (** equality function on hypothesis contexts *)
   let eq_named_context_val sigma1 sigma2 ctx1 ctx2 =
-    let open Environ in
-    let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in
+    let c1 = EConstr.named_context_of_val ctx1 and c2 = EConstr.named_context_of_val ctx2 in
     let eq_named_declaration d1 d2 =
       match d1, d2 with
       | LocalAssum (i1,t1), LocalAssum (i2,t2) ->
@@ -1101,7 +1100,7 @@ module Goal = struct
   let gmake_with info env sigma goal state =
     { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ;
       sigma = sigma ;
-      concl = EConstr.of_constr (Evd.evar_concl info);
+      concl = Evd.evar_concl info;
       state = state ;
       self = goal }
 
diff --git a/engine/termops.ml b/engine/termops.ml
index b7531f6fc..df43be28e 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -115,7 +115,7 @@ let pr_evar_suggested_name evk sigma =
   | _,Evar_kinds.GoalEvar -> Id.of_string "Goal"
   | _ ->
       let env = reset_with_named_context evi.evar_hyps (Global.env()) in
-      Namegen.id_of_name_using_hdchar env sigma (EConstr.of_constr evi.evar_concl) Anonymous
+      Namegen.id_of_name_using_hdchar env sigma evi.evar_concl Anonymous
   in
   let names = EvMap.mapi base_id (undefined_map sigma) in
   let id = EvMap.find evk names in
@@ -154,7 +154,7 @@ let protect f x =
   with e -> str "EXCEPTION: " ++ str (Printexc.to_string e)
 
 let print_kconstr a =
-  protect (fun c -> print_constr (EConstr.of_constr c)) a
+  protect (fun c -> print_constr c) a
 
 let pr_meta_map evd =
   let open Evd in
@@ -197,11 +197,11 @@ let pr_evar_source = function
       let print_constr = print_kconstr in
       let id = Option.get ido in
       str "parameter " ++ Id.print id ++ spc () ++ str "of" ++
-      spc () ++ print_constr (printable_constr_of_global c)
+      spc () ++ print_constr (EConstr.of_constr @@ printable_constr_of_global c)
   | Evar_kinds.InternalHole -> str "internal placeholder"
   | Evar_kinds.TomatchTypeParameter (ind,n) ->
       let print_constr = print_kconstr in
-      pr_nth n ++ str " argument of type " ++ print_constr (mkInd ind)
+      pr_nth n ++ str " argument of type " ++ print_constr (EConstr.mkInd ind)
   | Evar_kinds.GoalEvar -> str "goal evar"
   | Evar_kinds.ImpossibleCase -> str "type of impossible pattern-matching clause"
   | Evar_kinds.MatchingVar _ -> str "matching variable"
@@ -256,7 +256,7 @@ let compute_evar_dependency_graph sigma =
     in
     match evar_body evi with
     | Evar_empty -> acc
-    | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term c) acc
+    | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term (EConstr.Unsafe.to_constr c)) acc
   in
   Evd.fold fold sigma EvMap.empty
 
@@ -314,7 +314,8 @@ let print_env_short env =
   let print_constr = print_kconstr in
   let pr_rel_decl = function
     | RelDecl.LocalAssum (n,_) -> Name.print n
-    | RelDecl.LocalDef (n,b,_) -> str "(" ++ Name.print n ++ str " := " ++ print_constr b ++ str ")"
+    | RelDecl.LocalDef (n,b,_) -> str "(" ++ Name.print n ++ str " := "
+                                  ++ print_constr (EConstr.of_constr b) ++ str ")"
   in
   let pr_named_decl = NamedDecl.to_rel_decl %> pr_rel_decl in
   let nc = List.rev (named_context env) in
@@ -335,11 +336,11 @@ let pr_evar_constraints sigma pbs =
       Namegen.make_all_name_different env sigma
     in
     print_env_short env ++ spc () ++ str "|-" ++ spc () ++
-      protect (print_constr_env env sigma) (EConstr.of_constr t1) ++ spc () ++
+      protect (print_constr_env env sigma) t1 ++ spc () ++
       str (match pbty with
             | Reduction.CONV -> "=="
             | Reduction.CUMUL -> "<=") ++
-      spc () ++ protect (print_constr_env env Evd.empty) (EConstr.of_constr t2)
+      spc () ++ protect (print_constr_env env Evd.empty) t2
   in
   prlist_with_sep fnl pr_evconstr pbs