Promote evar_defs to evar_map (in Evd)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12502 85f007b7-540e-0410-9357-904b9bb8a0f7

19 files changed, 164 insertions, 165 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index fbc8bcd07a..ae7106fb3c 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -88,7 +88,7 @@ let coq_unit_judge =
 module type S = sig
   val compile_cases :
     loc -> case_style ->
-    (type_constraint -> env -> evar_defs ref -> rawconstr -> unsafe_judgment) * evar_defs ref ->
+    (type_constraint -> env -> evar_map ref -> rawconstr -> unsafe_judgment) * evar_map ref ->
     type_constraint ->
     env -> rawconstr option * tomatch_tuples * cases_clauses ->
     unsafe_judgment
@@ -291,14 +291,14 @@ let push_history_pattern n current cont =
 
 type 'a pattern_matching_problem =
     { env       : env;
-      evdref    : evar_defs ref;
+      evdref    : evar_map ref;
       pred      : constr;
       tomatch   : tomatch_stack;
       history   : pattern_continuation;
       mat       : 'a matrix;
       caseloc   : loc;
       casestyle : case_style;
-      typing_function: type_constraint -> env -> evar_defs ref -> 'a option -> unsafe_judgment }
+      typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment }
 
 (*--------------------------------------------------------------------------*
  * A few functions to infer the inductive type from the patterns instead of *
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index e6d42e10d9..6692403124 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -64,7 +64,7 @@ type tomatch_status =
 module type S = sig
   val compile_cases :
     loc -> case_style ->
-    (type_constraint -> env -> evar_defs ref -> rawconstr -> unsafe_judgment) * evar_defs ref ->
+    (type_constraint -> env -> evar_map ref -> rawconstr -> unsafe_judgment) * evar_map ref ->
     type_constraint ->
     env -> rawconstr option * tomatch_tuples * cases_clauses ->
     unsafe_judgment
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 5e4e7558c4..79b0c5a026 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -40,7 +40,7 @@ let pf_concl gl = gl.it.evar_concl
 
 type clausenv = {
   env      : env;
-  evd      : evar_defs;
+  evd      : evar_map;
   templval : constr freelisted;
   templtyp : constr freelisted }
 
@@ -477,4 +477,4 @@ let pr_clenv clenv =
   h 0
     (str"TEMPL: " ++ print_constr clenv.templval.rebus ++
      str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++
-     pr_evar_defs clenv.evd)
+     pr_evar_map clenv.evd)
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index 8e4dba5b5d..5571efbc57 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -32,7 +32,7 @@ open Unification
  *)
 type clausenv = {
   env      : env;
-  evd      : evar_defs;
+  evd      : evar_map;
   templval : constr freelisted;
   templtyp : constr freelisted }
 
@@ -122,12 +122,12 @@ val make_clenv_binding :
    [ccl] is [Meta n1=Meta n2]; if [n] is [Some 1], [lmetas] is [Meta n1]
    and [ccl] is [forall y, Meta n1=y -> y=Meta n1] *)
 val clenv_environments :
- evar_defs -> int option -> types -> evar_defs * constr list * types
+ evar_map -> int option -> types -> evar_map * constr list * types
 
 (* [clenv_environments_evars env sigma n t] does the same but returns
    a list of Evar's defined in [env] and extends [sigma] accordingly *)
 val clenv_environments_evars :
- env -> evar_defs -> int option -> types -> evar_defs * constr list * types
+ env -> evar_map -> int option -> types -> evar_map * constr list * types
 
 (* [clenv_conv_leq env sigma t c n] looks for c1...cn s.t. [t <= c c1...cn] *)
 val clenv_conv_leq :
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 2f5099c1a6..9f0b435216 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -29,38 +29,38 @@ module type S = sig
      inserts a coercion into [j], if needed, in such a way it gets as
      type a product; it returns [j] if no coercion is applicable *)
   val inh_app_fun :
-    env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment
+    env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment
 
   (* [inh_coerce_to_sort env evd j] coerces [j] to a type; i.e. it
      inserts a coercion into [j], if needed, in such a way it gets as
      type a sort; it fails if no coercion is applicable *)
   val inh_coerce_to_sort : loc ->
-    env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_type_judgment
+    env -> evar_map -> unsafe_judgment -> evar_map * unsafe_type_judgment
 
   (* [inh_coerce_to_base env evd j] coerces [j] to its base type; i.e. it
      inserts a coercion into [j], if needed, in such a way it gets as
      type its base type (the notion depends on the coercion system) *)
   val inh_coerce_to_base : loc ->
-    env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment
+    env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment
 
   (* [inh_coerce_to_prod env evars t] coerces [t] to a product type *)
   val inh_coerce_to_prod : loc ->
-    env -> evar_defs -> type_constraint_type -> evar_defs * type_constraint_type
+    env -> evar_map -> type_constraint_type -> evar_map * type_constraint_type
 
   (* [inh_conv_coerce_to loc env evd j t] coerces [j] to an object of type
      [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
      [j.uj_type] are convertible; it fails if no coercion is applicable *)
   val inh_conv_coerce_to : loc ->
-    env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment
+    env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment
 
   val inh_conv_coerce_rigid_to : loc ->
-    env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment
+    env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment
 
   (* [inh_conv_coerces_to loc env evd t t'] checks if an object of type [t]
      is coercible to an object of type [t'] adding evar constraints if needed;
      it fails if no coercion exists *)
   val inh_conv_coerces_to : loc ->
-    env -> evar_defs -> types -> type_constraint_type -> evar_defs
+    env -> evar_map -> types -> type_constraint_type -> evar_map
 
   (* [inh_pattern_coerce_to loc env evd pat ind1 ind2] coerces the Cases
      pattern [pat] typed in [ind1] into a pattern typed in [ind2];
@@ -231,7 +231,7 @@ module Default = struct
   let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true
 
 
-    let inh_conv_coerces_to loc env (evd : evar_defs) t (abs, t') = evd
+    let inh_conv_coerces_to loc env (evd : evar_map) t (abs, t') = evd
       (* Still problematic, as it changes unification
       let nabsinit, nabs =
 	match abs with
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 0329cc07c5..565cf0c409 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -26,38 +26,38 @@ module type S = sig
      inserts a coercion into [j], if needed, in such a way it gets as
      type a product; it returns [j] if no coercion is applicable *)
   val inh_app_fun :
-    env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment
+    env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment
 
   (* [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it
      inserts a coercion into [j], if needed, in such a way it gets as
      type a sort; it fails if no coercion is applicable *)
   val inh_coerce_to_sort : loc ->
-    env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_type_judgment
+    env -> evar_map -> unsafe_judgment -> evar_map * unsafe_type_judgment
 
   (* [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it
      inserts a coercion into [j], if needed, in such a way it gets as
      type its base type (the notion depends on the coercion system) *)
   val inh_coerce_to_base : loc ->
-    env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment
+    env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment
 
   (* [inh_coerce_to_prod env isevars t] coerces [t] to a product type *)
   val inh_coerce_to_prod : loc ->
-    env -> evar_defs -> type_constraint_type -> evar_defs * type_constraint_type
+    env -> evar_map -> type_constraint_type -> evar_map * type_constraint_type
 
   (* [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type
      [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
      [j.uj_type] are convertible; it fails if no coercion is applicable *)
   val inh_conv_coerce_to : loc ->
-    env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment
+    env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment
 
   val inh_conv_coerce_rigid_to : loc ->
-    env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment
+    env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment
 
   (* [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
      is coercible to an object of type [t'] adding evar constraints if needed;
      it fails if no coercion exists *)
   val inh_conv_coerces_to : loc ->
-    env -> evar_defs -> types -> type_constraint_type -> evar_defs
+    env -> evar_map -> types -> type_constraint_type -> evar_map
 
   (* [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases
      pattern [pat] typed in [ind1] into a pattern typed in [ind2];
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index a85f0f7395..9a4247bc26 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -17,24 +17,24 @@ open Evd
 (*i*)
 
 (* returns exception Reduction.NotConvertible if not unifiable *)
-val the_conv_x     : env -> constr -> constr -> evar_defs -> evar_defs
-val the_conv_x_leq : env -> constr -> constr -> evar_defs -> evar_defs
+val the_conv_x     : env -> constr -> constr -> evar_map -> evar_map
+val the_conv_x_leq : env -> constr -> constr -> evar_map -> evar_map
 
 (* The same function resolving evars by side-effect and
    catching the exception *)
-val e_conv  : env -> evar_defs ref -> constr -> constr -> bool
-val e_cumul : env -> evar_defs ref -> constr -> constr -> bool
+val e_conv  : env -> evar_map ref -> constr -> constr -> bool
+val e_cumul : env -> evar_map ref -> constr -> constr -> bool
 
 (*i For debugging *)
 val evar_conv_x :
-  env -> evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool
+  env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool
 val evar_eqappr_x :
-  env -> evar_defs ->
+  env -> evar_map ->
     conv_pb -> constr * constr list -> constr * constr list ->
-      evar_defs * bool
+      evar_map * bool
 (*i*)
 
-val consider_remaining_unif_problems : env -> evar_defs -> evar_defs * bool
+val consider_remaining_unif_problems : env -> evar_map -> evar_map * bool
 
 val check_conv_record : constr * types list -> constr * types list ->
   constr * constr list * (constr list * constr list) *
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 1357c6ce30..0613a35016 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -79,7 +79,7 @@ let nf_evar_info evc info =
 let nf_evars evm = Evd.fold (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi))
 		     evm Evd.empty
 
-let nf_evar_defs evd = Evd.evars_reset_evd (nf_evars evd) evd
+let nf_evar_map evd = Evd.evars_reset_evd (nf_evars evd) evd
 
 let nf_isevar evd = nf_evar evd
 let j_nf_isevar evd = j_nf_evar evd
@@ -958,7 +958,7 @@ and evar_define ?(choose=false) env (evk,_ as ev) rhs evd =
       with e ->
         pperrnl
           (str "Ill-typed evar instantiation: " ++ fnl() ++
-           pr_evar_defs evd' ++ fnl() ++
+           pr_evar_map evd' ++ fnl() ++
            str "----> " ++ int ev ++ str " := " ++
            print_constr body);
         raise e in*)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index a5a87b9bdb..4bfef79983 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -34,10 +34,10 @@ val new_untyped_evar : unit -> existential_key
 (***********************************************************)
 (* Creating a fresh evar given their type and context *)
 val new_evar :
-  evar_defs -> env -> ?src:loc * hole_kind -> ?filter:bool list -> types -> evar_defs * constr
+  evar_map -> env -> ?src:loc * hole_kind -> ?filter:bool list -> types -> evar_map * constr
 (* the same with side-effects *)
 val e_new_evar :
-  evar_defs ref -> env -> ?src:loc * hole_kind -> ?filter:bool list -> types -> constr
+  evar_map ref -> env -> ?src:loc * hole_kind -> ?filter:bool list -> types -> constr
 
 (* Create a fresh evar in a context different from its definition context:
    [new_evar_instance sign evd ty inst] creates a new evar of context
@@ -46,7 +46,7 @@ val e_new_evar :
    of [inst] are typed in the occurrence context and their type (seen
    as a telescope) is [sign] *)
 val new_evar_instance :
- named_context_val -> evar_defs -> types -> ?src:loc * hole_kind -> ?filter:bool list -> constr list -> evar_defs * constr
+ named_context_val -> evar_map -> types -> ?src:loc * hole_kind -> ?filter:bool list -> constr list -> evar_map * constr
 
 val make_pure_subst : evar_info -> constr array -> (identifier * constr) list
 
@@ -57,7 +57,7 @@ val make_pure_subst : evar_info -> constr array -> (identifier * constr) list
    possibly solving related unification problems, possibly leaving open
    some problems that cannot be solved in a unique way (except if choose is
    true); fails if the instance is not valid for the given [ev] *)
-val evar_define : ?choose:bool -> env -> existential -> constr -> evar_defs -> evar_defs
+val evar_define : ?choose:bool -> env -> existential -> constr -> evar_map -> evar_map
 
 (***********************************************************)
 (* Evars/Metas switching... *)
@@ -75,24 +75,24 @@ val non_instantiated : evar_map -> (evar * evar_info) list
 exception NoHeadEvar
 val head_evar : constr -> existential_key (* may raise NoHeadEvar *)
 
-val is_ground_term :  evar_defs -> constr -> bool
-val is_ground_env  :  evar_defs -> env -> bool
+val is_ground_term :  evar_map -> constr -> bool
+val is_ground_env  :  evar_map -> env -> bool
 val solve_refl :
-  (env ->  evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool)
-  -> env ->  evar_defs -> existential_key -> constr array -> constr array ->
-    evar_defs
+  (env ->  evar_map -> conv_pb -> constr -> constr -> evar_map * bool)
+  -> env ->  evar_map -> existential_key -> constr array -> constr array ->
+    evar_map
 val solve_simple_eqn :
-  (env ->  evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool)
-  -> ?choose:bool -> env ->  evar_defs -> bool option * existential * constr ->
-    evar_defs * bool
+  (env ->  evar_map -> conv_pb -> constr -> constr -> evar_map * bool)
+  -> ?choose:bool -> env ->  evar_map -> bool option * existential * constr ->
+    evar_map * bool
 
 (* [check_evars env initial_sigma extended_sigma c] fails if some
    new unresolved evar remains in [c] *)
-val check_evars : env -> evar_map -> evar_defs -> constr -> unit
+val check_evars : env -> evar_map -> evar_map -> constr -> unit
 
-val define_evar_as_product : evar_defs -> existential -> evar_defs * types
-val define_evar_as_lambda : evar_defs -> existential -> evar_defs * types
-val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts
+val define_evar_as_product : evar_map -> existential -> evar_map * types
+val define_evar_as_lambda : evar_map -> existential -> evar_map * types
+val define_evar_as_sort : evar_map -> existential -> evar_map * sorts
 
 val is_unification_pattern_evar : env -> existential -> constr list ->
   constr -> bool
@@ -123,8 +123,8 @@ val empty_valcon : val_constraint
 val mk_valcon : constr -> val_constraint
 
 val split_tycon :
-  loc -> env ->  evar_defs -> type_constraint ->
-    evar_defs * (name * type_constraint * type_constraint)
+  loc -> env ->  evar_map -> type_constraint ->
+    evar_map * (name * type_constraint * type_constraint)
 
 val valcon_of_tycon : type_constraint -> val_constraint
 
@@ -155,16 +155,16 @@ val nf_rel_context_evar : evar_map -> rel_context -> rel_context
 val nf_env_evar : evar_map -> env -> env
 
 (* Same for evar defs *)
-val nf_isevar :  evar_defs -> constr -> constr
-val j_nf_isevar :  evar_defs -> unsafe_judgment -> unsafe_judgment
+val nf_isevar :  evar_map -> constr -> constr
+val j_nf_isevar :  evar_map -> unsafe_judgment -> unsafe_judgment
 val jl_nf_isevar :
-   evar_defs -> unsafe_judgment list -> unsafe_judgment list
+   evar_map -> unsafe_judgment list -> unsafe_judgment list
 val jv_nf_isevar :
-   evar_defs -> unsafe_judgment array -> unsafe_judgment array
+   evar_map -> unsafe_judgment array -> unsafe_judgment array
 val tj_nf_isevar :
-   evar_defs -> unsafe_type_judgment -> unsafe_type_judgment
+   evar_map -> unsafe_type_judgment -> unsafe_type_judgment
 
-val nf_evar_defs : evar_defs -> evar_defs
+val nf_evar_map : evar_map -> evar_map
 
 (* Replacing all evars *)
 exception Uninstantiated_evar of existential_key
@@ -192,7 +192,7 @@ type clear_dependency_error =
 
 exception ClearDependencyError of identifier * clear_dependency_error
 
-val clear_hyps_in_evi : evar_defs ref -> named_context_val -> types ->
+val clear_hyps_in_evi : evar_map ref -> named_context_val -> types ->
   identifier list -> named_context_val * types
 
 val push_rel_context_to_named_context : Environ.env -> types -> 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index c96cc20cf9..1c47b8b00d 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -67,7 +67,7 @@ let eq_evar_info ei1 ei2 =
       - ExistentialMap ( Maps of existential_keys )
       - EvarInfoMap ( .t = evar_info ExistentialMap.t )
       - EvarMap ( .t = EvarInfoMap.t * sort_constraints )
-      - evar_defs (exported)
+      - evar_map (exported)
 *)
 
 module ExistentialMap = Intmap
@@ -418,7 +418,7 @@ type hole_kind =
 
 type conv_pb = Reduction.conv_pb
 type evar_constraint = conv_pb * Environ.env * constr * constr
-type evar_defs =
+type evar_map =
     { evars : EvarMap.t;
       conv_pbs : evar_constraint list;
       last_mods : ExistentialSet.t;
@@ -426,14 +426,14 @@ type evar_defs =
       metas : clbinding Metamap.t }
 
 (*** Lifting primitive from EvarMap. ***)
-type evar_map = evar_defs
+
 (* spiwack: this function seems to be used only for the definition of the progress
     tactical. I would recommand not using it in other places. *)
 let eq_evar_map d1 d2 =
   EvarMap.eq_evar_map d1.evars d2.evars
 
 (* spiwack: tentative. It might very well not be the semantics we want
-     for merging evar_defs *)
+     for merging evar_map *)
 let merge d1 d2 = {
 (* d1 with evars = EvarMap.merge d1.evars d2.evars*)
   evars = EvarMap.merge d1.evars d2.evars ;
@@ -447,10 +447,10 @@ let remove d e = { d with evars=EvarMap.remove d.evars e }
 let dom d = EvarMap.dom d.evars
 let find d e = EvarMap.find d.evars e
 let mem d e = EvarMap.mem d.evars e
-(* spiwack: this function loses information from the original evar_defs
+(* spiwack: this function loses information from the original evar_map
    it might be an idea not to export it. *)
 let to_list d = EvarMap.to_list d.evars
-(* spiwack: not clear what folding over an evar_defs, for now we shall
+(* spiwack: not clear what folding over an evar_map, for now we shall
     simply fold over the inner evar_map. *)
 let fold f d a = EvarMap.fold f d.evars a
 let is_evar d e = EvarMap.is_evar d.evars e
@@ -462,7 +462,7 @@ let existential_opt_value d e = EvarMap.existential_opt_value d.evars e
 
 (*** /Lifting... ***)
 
-(* evar_defs are considered empty disregarding histories *)
+(* evar_map are considered empty disregarding histories *)
 let is_empty d =
   d.evars = EvarMap.empty &&
   d.conv_pbs = [] &&
@@ -790,7 +790,7 @@ let pr_evar_info evi =
   in
   hov 2 (str"["  ++ phyps ++ spc () ++ str"|- "  ++ pty ++ pb ++ str"]")
 
-let pr_evar_defs_t (evars,cstrs as sigma) =
+let pr_evar_map_t (evars,cstrs as sigma) =
   let evs =
     if evars = EvarInfoMap.empty then mt ()
     else
@@ -813,10 +813,10 @@ let pr_constraints pbs =
 	| Reduction.CUMUL -> "<=") ++
       spc() ++ print_constr t2) pbs)
 
-let pr_evar_defs evd =
+let pr_evar_map evd =
   let pp_evm =
     if evd.evars = EvarMap.empty then mt() else
-      pr_evar_defs_t evd.evars++fnl() in
+      pr_evar_map_t evd.evars++fnl() in
   let cstrs =
     if evd.conv_pbs = [] then mt() else
     str"CONSTRAINTS:"++brk(0,1)++pr_constraints evd.conv_pbs++fnl() in
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index bcada1fc00..bffcf1cc64 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -79,7 +79,7 @@ val map_clb : (constr -> constr) -> clbinding -> clbinding
 (*********************************************************************)
 (*** Existential variables and unification states ***)
 
-(* A unification state (of type [evar_defs]) is primarily a finite mapping
+(* A unification state (of type [evar_map]) is primarily a finite mapping
     from existential variables to records containing the type of the evar
    ([evar_concl]), the context under which it was introduced ([evar_hyps])
    and its definition ([evar_body]). [evar_extra] is used to add any other
@@ -117,47 +117,47 @@ val evar_unfiltered_env :  evar_info -> env
 val evar_env :  evar_info -> env
 
 (*** Unification state ***)
-type evar_defs
+type evar_map
 
 (* Unification state and existential variables *)
 
 (* spiwack: this function seems to be used only for the definition of the progress
     tactical. I would recommand not using it in other places. *)
-val eq_evar_map : evar_defs -> evar_defs -> bool
+val eq_evar_map : evar_map -> evar_map -> bool
 
-val empty : evar_defs
-val is_empty : evar_defs -> bool
+val empty : evar_map
+val is_empty : evar_map -> bool
 
-val add : evar_defs -> evar -> evar_info -> evar_defs
+val add : evar_map -> evar -> evar_info -> evar_map
 
-val dom : evar_defs -> evar list
-val find : evar_defs -> evar -> evar_info
-val remove : evar_defs -> evar -> evar_defs
-val mem : evar_defs -> evar -> bool
-val to_list : evar_defs -> (evar * evar_info) list
-val fold : (evar -> evar_info -> 'a -> 'a) -> evar_defs -> 'a -> 'a
+val dom : evar_map -> evar list
+val find : evar_map -> evar -> evar_info
+val remove : evar_map -> evar -> evar_map
+val mem : evar_map -> evar -> bool
+val to_list : evar_map -> (evar * evar_info) list
+val fold : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
 
-val merge : evar_defs -> evar_defs -> evar_defs
+val merge : evar_map -> evar_map -> evar_map
 
-val define : evar -> constr -> evar_defs -> evar_defs
+val define : evar -> constr -> evar_map -> evar_map
 
-val is_evar : evar_defs -> evar -> bool
+val is_evar : evar_map -> evar -> bool
 
-val is_defined : evar_defs -> evar -> bool
+val is_defined : evar_map -> evar -> bool
 
 (*s [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has
     no body and [Not_found] if it does not exist in [sigma] *)
 
 exception NotInstantiatedEvar
-val existential_value : evar_defs -> existential -> constr
-val existential_type : evar_defs -> existential -> types
-val existential_opt_value : evar_defs -> existential -> constr option
+val existential_value : evar_map -> existential -> constr
+val existential_type : evar_map -> existential -> types
+val existential_opt_value : evar_map -> existential -> constr option
 
 (* Assume empty universe constraints in [evar_map] and [conv_pbs] *)
-val subst_evar_defs_light : substitution -> evar_defs -> evar_defs
+val subst_evar_defs_light : substitution -> evar_map -> evar_map
 
 (* spiwack: this function seems to somewhat break the abstraction. *)
-val evars_reset_evd  : evar_defs ->  evar_defs -> evar_defs
+val evars_reset_evd  : evar_map ->  evar_map -> evar_map
 
 
 
@@ -180,81 +180,81 @@ type hole_kind =
 
 (* spiwack: [is_undefined_evar] should be considered a candidate
                    for moving to evarutils *)
-val is_undefined_evar :  evar_defs -> constr -> bool
-val undefined_evars : evar_defs -> evar_defs
+val is_undefined_evar :  evar_map -> constr -> bool
+val undefined_evars : evar_map -> evar_map
 val evar_declare :
   named_context_val -> evar -> types -> ?src:loc * hole_kind ->
-      ?filter:bool list -> evar_defs -> evar_defs
-val evar_source : existential_key -> evar_defs -> loc * hole_kind
+      ?filter:bool list -> evar_map -> evar_map
+val evar_source : existential_key -> evar_map -> loc * hole_kind
 
 (* spiwack: this function seems to somewhat break the abstraction. *)
 (* [evar_merge evd ev1] extends the evars of [evd] with [evd1] *)
-val evar_merge : evar_defs -> evar_defs -> evar_defs
+val evar_merge : evar_map -> evar_map -> evar_map
 
 (* Unification constraints *)
 type conv_pb = Reduction.conv_pb
 type evar_constraint = conv_pb * env * constr * constr
-val add_conv_pb :  evar_constraint -> evar_defs -> evar_defs
+val add_conv_pb :  evar_constraint -> evar_map -> evar_map
 
 module ExistentialSet : Set.S with type elt = existential_key
-val extract_changed_conv_pbs : evar_defs ->
+val extract_changed_conv_pbs : evar_map ->
       (ExistentialSet.t -> evar_constraint -> bool) ->
-      evar_defs * evar_constraint list
-val extract_all_conv_pbs : evar_defs -> evar_defs * evar_constraint list
+      evar_map * evar_constraint list
+val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list
 
 
 (* Metas *)
-val find_meta : evar_defs -> metavariable -> clbinding
-val meta_list : evar_defs -> (metavariable * clbinding) list
-val meta_defined : evar_defs -> metavariable -> bool
+val find_meta : evar_map -> metavariable -> clbinding
+val meta_list : evar_map -> (metavariable * clbinding) list
+val meta_defined : evar_map -> metavariable -> bool
 (* [meta_fvalue] raises [Not_found] if meta not in map or [Anomaly] if
    meta has no value *)
-val meta_value     : evar_defs -> metavariable -> constr
-val meta_fvalue    : evar_defs -> metavariable -> constr freelisted * instance_status
-val meta_opt_fvalue : evar_defs -> metavariable -> (constr freelisted * instance_status) option
-val meta_type      : evar_defs -> metavariable -> types
-val meta_ftype     : evar_defs -> metavariable -> types freelisted
-val meta_name      : evar_defs -> metavariable -> name
-val meta_with_name : evar_defs -> identifier -> metavariable
+val meta_value     : evar_map -> metavariable -> constr
+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_name      : evar_map -> metavariable -> name
+val meta_with_name : evar_map -> identifier -> metavariable
 val meta_declare   :
-  metavariable -> types -> ?name:name -> evar_defs -> evar_defs
-val meta_assign    : metavariable -> constr * instance_status -> evar_defs -> evar_defs
-val meta_reassign  : metavariable -> constr * instance_status -> evar_defs -> evar_defs
+  metavariable -> types -> ?name:name -> 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
 
 (* [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *)
-val meta_merge : evar_defs -> evar_defs -> evar_defs
+val meta_merge : evar_map -> evar_map -> evar_map
 
-val undefined_metas : evar_defs -> metavariable list
-val metas_of : evar_defs -> meta_type_map
-val map_metas_fvalue : (constr -> constr) -> evar_defs -> evar_defs
+val undefined_metas : evar_map -> metavariable list
+val metas_of : evar_map -> meta_type_map
+val map_metas_fvalue : (constr -> constr) -> evar_map -> evar_map
 
 type metabinding = metavariable * constr * instance_status
 
-val retract_coercible_metas : evar_defs -> metabinding list * evar_defs
+val retract_coercible_metas : evar_map -> metabinding list * evar_map
 val subst_defined_metas : metabinding list -> constr -> constr option
 
 (**********************************************************)
 (* Sort variables *)
 
-val new_sort_variable : evar_defs -> sorts * evar_defs
-val is_sort_variable : evar_defs -> sorts -> bool
-val whd_sort_variable : evar_defs -> constr -> constr
-val set_leq_sort_variable : evar_defs -> sorts -> sorts -> evar_defs
-val define_sort_variable : evar_defs -> sorts -> sorts -> evar_defs
+val new_sort_variable : evar_map -> sorts * evar_map
+val is_sort_variable : evar_map -> sorts -> bool
+val whd_sort_variable : evar_map -> constr -> constr
+val set_leq_sort_variable : evar_map -> sorts -> sorts -> evar_map
+val define_sort_variable : evar_map -> sorts -> sorts -> evar_map
 
 (*********************************************************************)
 (* constr with holes *)
-type open_constr = evar_defs * constr
+type open_constr = evar_map * constr
 
 (*********************************************************************)
 (* The type constructor ['a sigma] adds an evar map to an object of
   type ['a] *)
 type 'a sigma = {
   it : 'a ;
-  sigma : evar_defs}
+  sigma : evar_map}
 
 val sig_it  : 'a sigma -> 'a
-val sig_sig : 'a sigma -> evar_defs
+val sig_sig : 'a sigma -> evar_map
 
 (**********************************************************)
 (* Failure explanation *)
@@ -265,16 +265,15 @@ type unsolvability_explanation = SeveralInstancesFound of int
 (* debug pretty-printer: *)
 
 val pr_evar_info : evar_info -> Pp.std_ppcmds
-val pr_evar_defs : evar_defs -> Pp.std_ppcmds
-val pr_sort_constraints : evar_defs -> Pp.std_ppcmds
+val pr_evar_map : evar_map -> Pp.std_ppcmds
+val pr_sort_constraints : evar_map -> Pp.std_ppcmds
 val pr_metaset : Metaset.t -> Pp.std_ppcmds
 
 
 (*** /!\Deprecated /!\ ***)
-type evar_map = evar_defs
-(* create an [evar_defs] with empty meta map: *)
-val create_evar_defs      : evar_defs -> evar_defs
-val create_goal_evar_defs : evar_defs -> evar_defs
-val is_defined_evar :  evar_defs -> existential -> bool
-val subst_evar_map : substitution -> evar_defs -> evar_defs
+(* create an [evar_map] with empty meta map: *)
+val create_evar_defs      : evar_map -> evar_map
+val create_goal_evar_defs : evar_map -> evar_map
+val is_defined_evar :  evar_map -> existential -> bool
+val subst_evar_map : substitution -> evar_map -> evar_map
 (*** /Deprecaded ***)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index eaa2e67576..10d9a1c4e2 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -101,7 +101,7 @@ sig
     evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr
 
   val understand_tcc_evars : ?fail_evar:bool -> ?resolve_classes:bool ->
-    evar_defs ref -> env -> typing_constraint -> rawconstr -> constr
+    evar_map ref -> env -> typing_constraint -> rawconstr -> constr
 
   (* More general entry point with evars from ltac *)
 
@@ -117,7 +117,7 @@ sig
 
   val understand_ltac :
     evar_map -> env -> var_map * unbound_ltac_var_map ->
-    typing_constraint -> rawconstr -> evar_defs * constr
+    typing_constraint -> rawconstr -> evar_map * constr
 
   (* Standard call to get a constr from a rawconstr, resolving implicit args *)
 
@@ -139,24 +139,24 @@ sig
 
   (* Idem but do not fail on unresolved evars *)
 
-  val understand_judgment_tcc : evar_defs ref -> env -> rawconstr -> unsafe_judgment
+  val understand_judgment_tcc : evar_map ref -> env -> rawconstr -> unsafe_judgment
 
   (*i*)
   (* Internal of Pretyping...
    * Unused outside, but useful for debugging
    *)
   val pretype :
-    type_constraint -> env -> evar_defs ref ->
+    type_constraint -> env -> evar_map ref ->
     var_map * (identifier * identifier option) list ->
     rawconstr -> unsafe_judgment
 
   val pretype_type :
-    val_constraint -> env -> evar_defs ref ->
+    val_constraint -> env -> evar_map ref ->
     var_map * (identifier * identifier option) list ->
     rawconstr -> unsafe_type_judgment
 
   val pretype_gen :
-    bool -> bool -> evar_defs ref -> env ->
+    bool -> bool -> evar_map ref -> env ->
     var_map * (identifier * identifier option) list ->
     typing_constraint -> rawconstr -> constr
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 7524c72a64..e3b18f73cb 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -44,7 +44,7 @@ sig
     evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr
 
   val understand_tcc_evars : ?fail_evar:bool -> ?resolve_classes:bool ->
-    evar_defs ref -> env -> typing_constraint -> rawconstr -> constr
+    evar_map ref -> env -> typing_constraint -> rawconstr -> constr
 
   (* More general entry point with evars from ltac *)
 
@@ -60,7 +60,7 @@ sig
 
   val understand_ltac :
     evar_map -> env -> var_map * unbound_ltac_var_map ->
-    typing_constraint -> rawconstr -> evar_defs * constr
+    typing_constraint -> rawconstr -> evar_map * constr
 
   (* Standard call to get a constr from a rawconstr, resolving implicit args *)
 
@@ -81,23 +81,23 @@ sig
   val understand_judgment : evar_map -> env -> rawconstr -> unsafe_judgment
 
   (* Idem but do not fail on unresolved evars *)
-  val understand_judgment_tcc : evar_defs ref -> env -> rawconstr -> unsafe_judgment
+  val understand_judgment_tcc : evar_map ref -> env -> rawconstr -> unsafe_judgment
 
   (*i*)
   (* Internal of Pretyping...
    *)
   val pretype :
-    type_constraint -> env -> evar_defs ref ->
+    type_constraint -> env -> evar_map ref ->
     var_map * (identifier * identifier option) list ->
     rawconstr -> unsafe_judgment
 
   val pretype_type :
-    val_constraint -> env -> evar_defs ref ->
+    val_constraint -> env -> evar_map ref ->
     var_map * (identifier * identifier option) list ->
     rawconstr -> unsafe_type_judgment
 
   val pretype_gen :
-    bool -> bool -> evar_defs ref -> env ->
+    bool -> bool -> evar_map ref -> env ->
     var_map * (identifier * identifier option) list ->
     typing_constraint -> rawconstr -> constr
 
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 3c3190484a..1268a3f3b5 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -217,6 +217,6 @@ val head_unfold_under_prod : transparent_state -> reduction_function
 val whd_betaiota_deltazeta_for_iota_state :  state_reduction_function
 
 (*s Meta-related reduction functions *)
-val meta_instance : evar_defs -> constr freelisted -> constr
-val nf_meta       : evar_defs -> constr -> constr
-val meta_reducible_instance : evar_defs -> constr freelisted -> constr
+val meta_instance : evar_map -> constr freelisted -> constr
+val nf_meta       : evar_map -> constr -> constr
+val meta_reducible_instance : evar_map -> constr freelisted -> constr
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 19ec47cf45..997b28c105 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -87,7 +87,7 @@ val mark_unresolvables : evar_map -> evar_map
 val is_class_evar : evar_map -> evar_info -> bool
 
 val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool ->
-  env -> evar_defs -> evar_defs
+  env -> evar_map -> evar_map
 val resolve_one_typeclass : env -> evar_map -> types -> open_constr
 
 val register_set_typeclass_transparency : (evaluable_global_reference -> bool -> unit) -> unit
@@ -96,5 +96,5 @@ val set_typeclass_transparency : evaluable_global_reference -> bool -> unit
 val register_add_instance_hint : (global_reference -> int option -> unit) -> unit
 val add_instance_hint : global_reference -> int option -> unit
 
-val solve_instanciations_problem : (env -> evar_defs -> bool -> bool -> bool -> evar_defs) ref
+val solve_instanciations_problem : (env -> evar_map -> bool -> bool -> bool -> evar_map) ref
 val solve_instanciation_problem : (env -> evar_map -> types -> open_constr) ref
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index ae9dec97f3..1de8b7a5fb 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -28,7 +28,7 @@ type typeclass_error =
     | NotAClass of constr
     | UnboundMethod of global_reference * identifier located (* Class name, method *)
     | NoInstance of identifier located * constr list
-    | UnsatisfiableConstraints of evar_defs * (existential_key * hole_kind) option
+    | UnsatisfiableConstraints of evar_map * (existential_key * hole_kind) option
     | MismatchedContextInstance of contexts * constr_expr list * rel_context (* found, expected *)
 
 exception TypeClassError of env * typeclass_error
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 5cf8508901..7fd04e225d 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -28,7 +28,7 @@ type typeclass_error =
   | NotAClass of constr
   | UnboundMethod of global_reference * identifier located (* Class name, method *)
   | NoInstance of identifier located * constr list
-  | UnsatisfiableConstraints of evar_defs * (existential_key * hole_kind) option
+  | UnsatisfiableConstraints of evar_map * (existential_key * hole_kind) option
   | MismatchedContextInstance of contexts * constr_expr list * rel_context (* found, expected *)
 
 exception TypeClassError of env * typeclass_error
@@ -39,7 +39,7 @@ val unbound_method : env -> global_reference -> identifier located -> 'a
 
 val no_instance : env -> identifier located -> constr list -> 'a
 
-val unsatisfiable_constraints : env -> evar_defs -> evar option -> 'a
+val unsatisfiable_constraints : env -> evar_map -> evar option -> 'a
 
 val mismatched_ctx_inst : env -> contexts -> constr_expr list -> rel_context -> 'a
 
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 0aa65bef38..9a40d01ec9 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -25,10 +25,10 @@ val sort_of : env -> evar_map -> types -> sorts
 val check   : env -> evar_map -> constr -> types -> unit
 
 (* The same but with metas... *)
-val mtype_of : env -> evar_defs -> constr -> types
-val msort_of : env -> evar_defs -> types -> sorts
-val mcheck   : env -> evar_defs -> constr -> types -> unit
-val meta_type : evar_defs -> metavariable -> types
+val mtype_of : env -> evar_map -> constr -> types
+val msort_of : env -> evar_map -> types -> sorts
+val mcheck   : env -> evar_map -> constr -> types -> unit
+val meta_type : evar_map -> metavariable -> types
 
 (* unused typing function... *)
-val mtype_of_type : env -> evar_defs -> types -> types
+val mtype_of_type : env -> evar_map -> types -> types
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 2df1c648a4..cc62a9bb81 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -27,23 +27,23 @@ val default_no_delta_unify_flags : unify_flags
 
 (* The "unique" unification fonction *)
 val w_unify :
-  bool -> env -> conv_pb -> ?flags:unify_flags -> constr -> constr -> evar_defs -> evar_defs
+  bool -> env -> conv_pb -> ?flags:unify_flags -> constr -> constr -> evar_map -> evar_map
 
 (* [w_unify_to_subterm env (c,t) m] performs unification of [c] with a
    subterm of [t]. Constraints are added to [m] and the matched
    subterm of [t] is also returned. *)
 val w_unify_to_subterm :
-  env -> ?flags:unify_flags -> constr * constr -> evar_defs -> evar_defs * constr
+  env -> ?flags:unify_flags -> constr * constr -> evar_map -> evar_map * constr
 
 val w_unify_to_subterm_all :
-  env -> ?flags:unify_flags -> constr * constr -> evar_defs -> (evar_defs * constr) list
+  env -> ?flags:unify_flags -> constr * constr -> evar_map -> (evar_map * constr) list
 
-val w_unify_meta_types : env -> ?flags:unify_flags -> evar_defs -> evar_defs
+val w_unify_meta_types : env -> ?flags:unify_flags -> evar_map -> evar_map
 
 (* [w_coerce_to_type env evd c ctyp typ] tries to coerce [c] of type
    [ctyp] so that its gets type [typ]; [typ] may contain metavariables *)
-val w_coerce_to_type : env -> evar_defs -> constr -> types -> types ->
-  evar_defs * constr
+val w_coerce_to_type : env -> evar_map -> constr -> types -> types ->
+  evar_map * constr
 
 (*i This should be in another module i*)
 
@@ -51,4 +51,4 @@ val w_coerce_to_type : env -> evar_defs -> constr -> types -> types ->
 (* abstracts the terms in l over c to get a term of type t *)
 (* (exported for inv.ml) *)
 val abstract_list_all :
-  env -> evar_defs -> constr -> constr -> constr list -> constr
+  env -> evar_map -> constr -> constr -> constr list -> constr