On remplace evar_map par evar_defs (seul evar_defs est désormais exporté

par Evd). Ça s'accompagne de quelques autres modifications de 
l'interface (certaines fonctions étaient des doublons, ou des 
conversions entre evar_map et evar_defs).

J'ai modifié un peu la structure de evd.ml aussi, pour éviter des 
fonctions redéfinies deux fois (i.e. définies trois fois !), j'ai 
introduit des sous-modules pour les différentes couches.

Il y a à l'heure actuelle une pénalité en performance assez sévère (due 
principalement à la nouvelle mouture de Evd.merge, si mon diagnostique 
est correct). Mais fera l'objet de plusieurs optimisations dans les 
commits à venir.

Un peu plus ennuyeux, la test-suite du mode déclaratif ne passe plus. Un 
appel de Decl_proof_instr.mark_as_done visiblement, je suis pour 
l'instant incapable de comprendre ce qui cause cette erreur. J'espère 
qu'on pourra le déterminer rapidement.

Ce commit est le tout premier commit dans le trunk en rapport avec les 
évolution futures de la machine de preuve, en vue en particulier 
d'obtenir un "vrai refine".



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

13 files changed, 504 insertions, 420 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index dcedfa51d5..8451d1285a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -363,7 +363,7 @@ let unify_tomatch_with_patterns evdref env loc typ pats realnames =
     | None -> NotInd (None,typ)
     | Some (_,(ind,_)) ->
 	inh_coerce_to_ind evdref env typ ind;
-	try try_find_ind env (evars_of !evdref) typ realnames
+	try try_find_ind env ( !evdref) typ realnames
 	with Not_found -> NotInd (None,typ)
 
 let find_tomatch_tycon evdref env loc = function
@@ -377,9 +377,9 @@ let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) =
   let loc = Some (loc_of_rawconstr tomatch) in
   let tycon,realnames = find_tomatch_tycon evdref env loc indopt in
   let j = typing_fun tycon env evdref tomatch in
-  let typ = nf_evar (evars_of !evdref) j.uj_type in
+  let typ = nf_evar ( !evdref) j.uj_type in
   let t =
-    try try_find_ind env (evars_of !evdref) typ realnames
+    try try_find_ind env ( !evdref) typ realnames
     with Not_found ->
       unify_tomatch_with_patterns evdref env loc typ pats realnames in
   (j.uj_val,t)
@@ -414,7 +414,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
   let typ,names =
     match typ with IsInd(t,_,names) -> t,Some names | NotInd(_,t) -> t,None in
   let typ =
-    try try_find_ind pb.env (evars_of !(pb.evdref)) typ names
+    try try_find_ind pb.env ( !(pb.evdref)) typ names
     with Not_found -> NotInd (None,typ) in
   let tomatch = ((current,typ),deps,dep) in
   match typ with
@@ -432,7 +432,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
 	      else
 		(evd_comb2 (Coercion.inh_conv_coerce_to dummy_loc pb.env)
 		  pb.evdref (make_judge current typ) (mk_tycon_type indt)).uj_val in
-	    let sigma = evars_of !(pb.evdref) in
+	    let sigma =  !(pb.evdref) in
 	    let typ = try_find_ind pb.env sigma indt names in
 	    ((current,typ),deps,dep))
   | _ -> tomatch
@@ -934,10 +934,10 @@ let expand_arg tms ccl ((_,t),_,na) =
 
 let adjust_impossible_cases pb pred tomatch submat =
   if submat = [] then
-    match kind_of_term (whd_evar (evars_of !(pb.evdref)) pred) with
+    match kind_of_term (whd_evar ( !(pb.evdref)) pred) with
     | Evar (evk,_) when snd (evar_source evk !(pb.evdref)) = ImpossibleCase ->
 	let default = (coq_unit_judge ()).uj_type in
-	pb.evdref := Evd.evar_define evk default !(pb.evdref);
+	pb.evdref := Evd.define evk default !(pb.evdref);
       (* we add an "assert false" case *)
       let pats = List.map (fun _ -> PatVar (dummy_loc,Anonymous)) tomatch in
       let aliasnames =
@@ -989,8 +989,8 @@ let specialize_predicate newtomatchs (names,(depna,_)) cs tms ccl =
   List.fold_left (expand_arg tms) ccl''' newtomatchs
 
 let find_predicate loc env evdref p current (IndType (indf,realargs)) dep tms =
-  let pred= abstract_predicate env (evars_of !evdref) indf current dep tms p in
-  (pred, whd_betaiota (evars_of !evdref)
+  let pred= abstract_predicate env ( !evdref) indf current dep tms p in
+  (pred, whd_betaiota ( !evdref)
            (applist (pred, realargs@[current])), new_Type ())
 
 let adjust_predicate_from_tomatch ((_,oldtyp),_,(nadep,_)) typ pb =
@@ -1068,7 +1068,7 @@ let rec generalize_problem names pb = function
 let build_leaf pb =
   let rhs = extract_rhs pb in
   let j = pb.typing_function (mk_tycon pb.pred) rhs.rhs_env pb.evdref rhs.it in
-  j_nf_evar (evars_of !(pb.evdref)) j
+  j_nf_evar ( !(pb.evdref)) j
 
 (* Building the sub-problem when all patterns are variables *)
 let shift_problem ((current,t),_,(nadep,_)) pb =
@@ -1236,7 +1236,7 @@ and compile_generalization pb d rest =
 and compile_alias pb (deppat,nondeppat,d,t) rest =
   let history = simplify_history pb.history in
   let sign, newenv, mat =
-    insert_aliases pb.env (evars_of !(pb.evdref)) (deppat,nondeppat,d,t) pb.mat in
+    insert_aliases pb.env ( !(pb.evdref)) (deppat,nondeppat,d,t) pb.mat in
   let n = List.length sign in
 
   (* We had Gamma1; x:current; Gamma2 |- tomatch(x) and we rebind x to get *)
@@ -1456,7 +1456,7 @@ let adjust_to_extended_env_and_remove_deps env extenv subst t =
 *)
 
 let abstract_tycon loc env evdref subst _tycon extenv t =
-  let sigma = evars_of !evdref in
+  let sigma =  !evdref in
   let t = nf_betaiota sigma t in (* it helps in some cases to remove K-redex *)
   let subst0,t0 = adjust_to_extended_env_and_remove_deps env extenv subst t in
   (* We traverse the type T of the original problem Xi looking for subterms
@@ -1503,7 +1503,7 @@ let build_tycon loc env tycon_env subst tycon extenv evdref t =
 	  e_new_evar evdref env ~src:(loc,ImpossibleCase) (new_Type ()) in
 	lift (n'-n) impossible_case_type
     | Some t -> abstract_tycon loc tycon_env evdref subst tycon extenv t in
-  get_judgment_of extenv (evars_of !evdref) t
+  get_judgment_of extenv ( !evdref) t
 
 (* For a multiple pattern-matching problem Xi on t1..tn with return
  * type T, [build_inversion_problem Gamma Sigma (t1..tn) T] builds a return
@@ -1516,7 +1516,7 @@ let build_tycon loc env tycon_env subst tycon extenv evdref t =
  *)
 
 let build_inversion_problem loc env evdref tms t =
-  let sigma = evars_of !evdref in
+  let sigma =  !evdref in
   let make_patvar t (subst,avoid) =
     let id = next_name_away (named_hd env t Anonymous) avoid in
     PatVar (dummy_loc,Name id), ((id,t)::subst, id::avoid) in
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 24f3b77260..05c64521a1 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -45,7 +45,7 @@ type clausenv = {
   templtyp : constr freelisted }
 
 let cl_env ce = ce.env
-let cl_sigma ce = evars_of ce.evd
+let cl_sigma ce =  ce.evd
 
 let subst_clenv sub clenv = 
   { templval = map_fl (subst_mps sub) clenv.templval;
@@ -129,7 +129,7 @@ let clenv_conv_leq env sigma t c bound =
   let evars,args,_ = clenv_environments_evars env evd (Some bound) ty in
   let evars = Evarconv.the_conv_x_leq env t (applist (c,args)) evars in
   let evars,_ = Evarconv.consider_remaining_unif_problems env evars in
-  let args = List.map (whd_evar (Evd.evars_of evars)) args in
+  let args = List.map (whd_evar ( evars)) args in
   check_evars env sigma evars (applist (c,args));
   args
 
@@ -254,7 +254,7 @@ let clenv_unify_meta_types ?(flags=default_unify_flags) clenv =
   { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
 
 let clenv_unique_resolver allow_K ?(flags=default_unify_flags) clenv gl =
-  if isMeta (fst (whd_stack (evars_of clenv.evd) clenv.templtyp.rebus)) then
+  if isMeta (fst (whd_stack ( clenv.evd) clenv.templtyp.rebus)) then
     clenv_unify allow_K CUMUL ~flags:flags (clenv_type clenv) (pf_concl gl)
       (clenv_unify_meta_types ~flags:flags clenv)
   else
@@ -341,7 +341,7 @@ let clenv_fchain ?(allow_K=true) ?(flags=default_unify_flags) mv clenv nextclenv
     { templval = clenv.templval;
       templtyp = clenv.templtyp;
       evd = 
-        evar_merge (meta_merge clenv.evd nextclenv.evd) (evars_of clenv.evd);
+        evar_merge (meta_merge clenv.evd nextclenv.evd) ( clenv.evd);
       env = nextclenv.env } in
   (* unify the type of the template of [nextclenv] with the type of [mv] *)
   let clenv'' =
@@ -402,7 +402,7 @@ let error_already_defined b =
           (str "Position " ++ int n ++ str" already defined.")
 
 let clenv_unify_binding_type clenv c t u =
-  if isMeta (fst (whd_stack (evars_of clenv.evd) u)) then
+  if isMeta (fst (whd_stack ( clenv.evd) u)) then
     (* Not enough information to know if some subtyping is needed *)
     CoerceToType, clenv, c
   else
@@ -416,7 +416,7 @@ let clenv_unify_binding_type clenv c t u =
 let clenv_assign_binding clenv k (sigma,c) =
   let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
   let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in
-  let c_typ = nf_betaiota (evars_of clenv'.evd) (clenv_get_type_of clenv' c) in
+  let c_typ = nf_betaiota ( clenv'.evd) (clenv_get_type_of clenv' c) in
   let status,clenv'',c = clenv_unify_binding_type clenv' c c_typ k_typ in
   { clenv'' with evd = meta_assign k (c,(UserGiven,status)) clenv''.evd }
 
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 85e14d482c..3a5f351255 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -123,7 +123,7 @@ module Default = struct
     with _ -> anomaly "apply_coercion"
 
   let inh_app_fun env evd j = 
-    let t = whd_betadeltaiota env (evars_of evd) j.uj_type in
+    let t = whd_betadeltaiota env ( evd) j.uj_type in
       match kind_of_term t with
 	| Prod (_,_,_) -> (evd,j)
 	| Evar ev ->
@@ -132,21 +132,21 @@ module Default = struct
 	| _ ->
        	    (try
       	       let t,p =
-		 lookup_path_to_fun_from env (evars_of evd) j.uj_type in
-		 (evd,apply_coercion env (evars_of evd) p j t)
+		 lookup_path_to_fun_from env ( evd) j.uj_type in
+		 (evd,apply_coercion env ( evd) p j t)
 	     with Not_found -> (evd,j))
 
   let inh_tosort_force loc env evd j =
     try
-      let t,p = lookup_path_to_sort_from env (evars_of evd) j.uj_type in
-      let j1 = apply_coercion env (evars_of evd) p j t in 
-      let j2 = on_judgment_type (whd_evar (evars_of evd)) j1 in
+      let t,p = lookup_path_to_sort_from env ( evd) j.uj_type in
+      let j1 = apply_coercion env ( evd) p j t in 
+      let j2 = on_judgment_type (whd_evar ( evd)) j1 in
         (evd,type_judgment env j2)
     with Not_found ->
-      error_not_a_type_loc loc env (evars_of evd) j
+      error_not_a_type_loc loc env ( evd) j
 
   let inh_coerce_to_sort loc env evd j =
-    let typ = whd_betadeltaiota env (evars_of evd) j.uj_type in
+    let typ = whd_betadeltaiota env ( evd) j.uj_type in
       match kind_of_term typ with
 	| Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s })
 	| Evar ev when not (is_defined_evar evd ev) ->
@@ -166,11 +166,11 @@ module Default = struct
     else
     let v', t' =
       try 
-	let t2,t1,p = lookup_path_between env (evars_of evd) (t,c1) in
+	let t2,t1,p = lookup_path_between env ( evd) (t,c1) in
 	  match v with
 	      Some v -> 
 		let j =
-		  apply_coercion env (evars_of evd) p
+		  apply_coercion env ( evd) p
 		    {uj_val = v; uj_type = t} t2 in
 		  Some j.uj_val, j.uj_type
 	    | None -> None, t
@@ -185,8 +185,8 @@ module Default = struct
     try inh_coerce_to_fail env evd rigidonly v t c1
     with NoCoercion ->
     match
-      kind_of_term (whd_betadeltaiota env (evars_of evd) t),
-      kind_of_term (whd_betadeltaiota env (evars_of evd) c1)
+      kind_of_term (whd_betadeltaiota env ( evd) t),
+      kind_of_term (whd_betadeltaiota env ( evd) c1)
     with
     | Prod (name,t1,t2), Prod (_,u1,u2) -> 
         (* Conversion did not work, we may succeed with a coercion. *)
@@ -215,7 +215,7 @@ module Default = struct
 	    try 
 	      inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
 	    with NoCoercion ->
-	      let sigma = evars_of evd in
+	      let sigma =  evd in
 		error_actual_type_loc loc env sigma cj t
 	  in
 	  let val' = match val' with Some v -> v | None -> assert(false) in
@@ -253,7 +253,7 @@ module Default = struct
 		  pi1 (inh_conv_coerce_to_fail loc env' evd None t t')
 		with NoCoercion ->
 		  evd) (* Maybe not enough information to unify *)
-	      (*let sigma = evars_of evd in
+	      (*let sigma =  evd in
 		error_cannot_coerce env' sigma (t, t'))*)
 	    else evd
 	with Invalid_argument _ -> evd	  *)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index d7da100abc..d185bd64ec 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -52,7 +52,7 @@ let eval_flexible_term env c =
   | _ -> assert false
 
 let evar_apprec env evd stack c =
-  let sigma = evars_of evd in
+  let sigma =  evd in
   let rec aux s =
     let (t,stack) = whd_betaiota_deltazeta_for_iota_state env sigma s in
     match kind_of_term t with
@@ -62,7 +62,7 @@ let evar_apprec env evd stack c =
   in aux (c, append_stack_list stack empty_stack)
 
 let apprec_nohdbeta env evd c =
-  match kind_of_term (fst (Reductionops.whd_stack (evars_of evd) c)) with
+  match kind_of_term (fst (Reductionops.whd_stack ( evd) c)) with
     | (Case _ | Fix _) -> applist (evar_apprec env evd [] c)
     | _ -> c
 
@@ -158,7 +158,7 @@ let ise_array2 evd f v1 v2 =
   else (evd,false)
 
 let rec evar_conv_x env evd pbty term1 term2 = 
-  let sigma = evars_of evd in
+  let sigma =  evd in
   let term1 = whd_castappevar sigma term1 in
   let term2 = whd_castappevar sigma term2 in
   (* Maybe convertible but since reducing can erase evars which [evar_apprec]
@@ -166,7 +166,7 @@ let rec evar_conv_x env evd pbty term1 term2 =
      Note: incomplete heuristic... *)
   let ground_test =
     if is_ground_term evd term1 && is_ground_term evd term2 then
-      if is_fconv pbty env (evars_of evd) term1 term2 then
+      if is_fconv pbty env ( evd) term1 term2 then
         Some true
       else if is_ground_env evd env then Some false
       else None
@@ -222,7 +222,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  then
 	    (* Miller-Pfenning's patterns unification *)
 	    (* Preserve generality (except that CCI has no eta-conversion) *)
-	    let t2 = nf_evar (evars_of evd) (applist appr2) in
+	    let t2 = nf_evar ( evd) (applist appr2) in
 	    let t2 = solve_pattern_eqn env l1 t2 in
 	    solve_simple_eqn evar_conv_x env evd (pbty,ev1,t2)
 	  else if
@@ -254,7 +254,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  then
 	    (* Miller-Pfenning's patterns unification *)
 	    (* Preserve generality (except that CCI has no eta-conversion) *)
-	    let t1 = nf_evar (evars_of evd) (applist appr1) in
+	    let t1 = nf_evar ( evd) (applist appr1) in
 	    let t1 = solve_pattern_eqn env l2 t1 in
 	    solve_simple_eqn evar_conv_x env evd (pbty,ev2,t1)
 	  else if
@@ -293,7 +293,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
              if the first argument is a beta-redex (expand a constant
              only if necessary) or the second argument is potentially
              usable as a canonical projection *)
-	  if isLambda flex1 or is_open_canonical_projection (evars_of i) appr2
+	  if isLambda flex1 or is_open_canonical_projection ( i) appr2
 	  then
 	    match eval_flexible_term env flex1 with
 	    | Some v1 ->
@@ -322,7 +322,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	then
 	  (* Miller-Pfenning's patterns unification *)
 	  (* Preserve generality (except that CCI has no eta-conversion) *)
-	  let t2 = nf_evar (evars_of evd) (applist appr2) in
+	  let t2 = nf_evar ( evd) (applist appr2) in
 	  let t2 = solve_pattern_eqn env l1 t2 in
 	  solve_simple_eqn evar_conv_x env evd (pbty,ev1,t2)
 	else
@@ -337,7 +337,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	then
 	  (* Miller-Pfenning's patterns unification *)
 	  (* Preserve generality (except that CCI has no eta-conversion) *)
-	  let t1 = nf_evar (evars_of evd) (applist appr1) in
+	  let t1 = nf_evar ( evd) (applist appr1) in
 	  let t1 = solve_pattern_eqn env l2 t1 in
 	  solve_simple_eqn evar_conv_x env evd (pbty,ev2,t1)
 	else
@@ -382,7 +382,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
             ise_and evd
               [(fun i -> evar_conv_x env i CONV c1 c2);
                (fun i ->
-                 let c = nf_evar (evars_of i) c1 in
+                 let c = nf_evar ( i) c1 in
                  evar_conv_x (push_rel (na,None,c) env) i CONV c'1 c'2)]
 
 	| LetIn (na,b1,t1,c'1), LetIn (_,b2,_,c'2) ->
@@ -390,8 +390,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
               ise_and i
                 [(fun i -> evar_conv_x env i CONV b1 b2);
                  (fun i ->
-                   let b = nf_evar (evars_of i) b1 in
-	           let t = nf_evar (evars_of i) t1 in
+                   let b = nf_evar ( i) b1 in
+	           let t = nf_evar ( i) t1 in
                    evar_conv_x (push_rel (na,Some b,t) env) i pbty c'1 c'2);
                  (fun i -> ise_list2 i
                      (fun i -> evar_conv_x env i CONV) l1 l2)]
@@ -414,7 +414,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
             ise_and evd
               [(fun i -> evar_conv_x env i CONV c1 c2);
                (fun i ->
- 	         let c = nf_evar (evars_of i) c1 in
+ 	         let c = nf_evar ( i) c1 in
 	         evar_conv_x (push_rel (n,None,c) env) i pbty c'1 c'2)]
 
 	| Ind sp1, Ind sp2 ->
@@ -508,15 +508,15 @@ let first_order_unification env evd (ev1,l1) (term2,l2) =
 	solve_simple_eqn evar_conv_x env i (CONV,ev1,t2))]
 
 let choose_less_dependent_instance evk evd term args =
-  let evi = Evd.find (evars_of evd) evk in
+  let evi = Evd.find ( evd) evk in
   let subst = make_pure_subst evi args in
   let subst' = List.filter (fun (id,c) -> c = term) subst in
   if subst' = [] then error "Too complex unification problem." else
-  Evd.evar_define evk (mkVar (fst (List.hd subst'))) evd
+  Evd.define evk (mkVar (fst (List.hd subst'))) evd
 
 let apply_conversion_problem_heuristic env evd pbty t1 t2 =
-  let t1 = apprec_nohdbeta env evd (whd_castappevar (evars_of evd) t1) in
-  let t2 = apprec_nohdbeta env evd (whd_castappevar (evars_of evd) t2) in
+  let t1 = apprec_nohdbeta env evd (whd_castappevar ( evd) t1) in
+  let t2 = apprec_nohdbeta env evd (whd_castappevar ( evd) t2) in
   let (term1,l1 as appr1) = decompose_app t1 in
   let (term2,l2 as appr2) = decompose_app t2 in
   match kind_of_term term1, kind_of_term term2 with
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 37288d394d..0ef2c63191 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -79,13 +79,13 @@ 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.evars_of evd)) evd
+let nf_evar_defs evd = Evd.evars_reset_evd (nf_evars ( evd)) evd
 
-let nf_isevar evd = nf_evar (Evd.evars_of evd)
-let j_nf_isevar evd = j_nf_evar (Evd.evars_of evd)
-let jl_nf_isevar evd = jl_nf_evar (Evd.evars_of evd)
-let jv_nf_isevar evd = jv_nf_evar (Evd.evars_of evd)
-let tj_nf_isevar evd = tj_nf_evar (Evd.evars_of evd)
+let nf_isevar evd = nf_evar ( evd)
+let j_nf_isevar evd = j_nf_evar ( evd)
+let jl_nf_isevar evd = jl_nf_evar ( evd)
+let jv_nf_isevar evd = jv_nf_evar ( evd)
+let tj_nf_isevar evd = tj_nf_evar ( evd)
 
 (**********************)
 (* Creating new metas *)
@@ -279,7 +279,7 @@ let evar_well_typed_body evd ev evi body =
   try
     let env = evar_unfiltered_env evi in
     let ty = evi.evar_concl in
-    Typing.check env (evars_of evd) body ty;
+    Typing.check env ( evd) body ty;
     true
   with e ->
     pperrnl
@@ -339,13 +339,13 @@ let shrink_context env subst ty =
   shrink_named subst [] rev_named_sign
 
 let extend_evar env evdref k (evk1,args1) c =
-  let ty = get_type_of env (evars_of !evdref) c in
+  let ty = get_type_of env ( !evdref) c in
   let overwrite_first v1 v2 =
     let v = Array.copy v1 in
     let n = Array.length v - Array.length v2 in
     for i = 0 to Array.length v2 - 1 do v.(n+i) <- v2.(i) done;
     v in
-  let evi1 = Evd.find (evars_of !evdref) evk1 in
+  let evi1 = Evd.find ( !evdref) evk1 in
   let named_sign',rel_sign',ty =
     if k = 0 then [], [], ty
     else shrink_context env (List.rev (make_pure_subst evi1 args1)) ty in
@@ -378,7 +378,7 @@ let restrict_upon_filter evd evi evk p args =
   if newfilter <> filter then
     let (evd,newev) = new_evar evd (evar_unfiltered_env evi) ~src:(evar_source evk evd)
 	~filter:newfilter evi.evar_concl in
-    let evd = Evd.evar_define evk newev evd in
+    let evd = Evd.define evk newev evd in
     evd,fst (destEvar newev),newargs
   else
     evd,evk,args
@@ -416,7 +416,7 @@ let rec check_and_clear_in_constr evdref err ids c =
       | Evar (evk,l as ev) -> 
 	  if Evd.is_defined_evar !evdref ev then
 	    (* If evk is already defined we replace it by its definition *)
-	    let nc = whd_evar (evars_of !evdref) c in 
+	    let nc = whd_evar ( !evdref) c in 
 	      (check_and_clear_in_constr evdref err ids nc)
 	  else 
 	    (* We check for dependencies to elements of ids in the
@@ -424,7 +424,7 @@ let rec check_and_clear_in_constr evdref err ids c =
 	       arguments. Concurrently, we build a new evar
 	       corresponding to e where hypotheses of ids have been
 	       removed *)
-	    let evi = Evd.find (evars_of !evdref) evk in
+	    let evi = Evd.find ( !evdref) evk in
 	    let ctxt = Evd.evar_filtered_context evi in
 	    let (nhyps,nargs,rids) =
 	      List.fold_right2 
@@ -455,7 +455,7 @@ let rec check_and_clear_in_constr evdref err ids c =
 
 	    let env = Sign.fold_named_context push_named nhyps ~init:(empty_env) in
 	    let ev'= e_new_evar evdref env ~src:(evar_source evk !evdref) nconcl in
-	      evdref := Evd.evar_define evk ev' !evdref;
+	      evdref := Evd.define evk ev' !evdref;
 	      let (evk',_) = destEvar ev' in
 		mkEvar(evk', Array.of_list nargs)
 
@@ -605,17 +605,17 @@ let project_with_effects env sigma effects t subst =
  * type is an evar too.
  *
  * Note: typing creates new evar problems, which induces a recursive dependency
- * with [evar_define]. To avoid a too large set of recursive functions, we
- * pass [evar_define] to [do_projection_effects] as a parameter.
+ * with [define]. To avoid a too large set of recursive functions, we
+ * pass [define] to [do_projection_effects] as a parameter.
  *)
 
 let rec do_projection_effects define_fun env ty evd = function
   | ProjectVar -> evd
   | ProjectEvar ((evk,argsv),evi,id,p) ->
-      let evd = Evd.evar_define evk (mkVar id) evd in
+      let evd = Evd.define evk (mkVar id) evd in
       (* TODO: simplify constraints involving evk *)
       let evd = do_projection_effects define_fun env ty evd p in
-      let ty = whd_betadeltaiota env (evars_of evd) (Lazy.force ty) in
+      let ty = whd_betadeltaiota env ( evd) (Lazy.force ty) in
       if not (isSort ty) then
 	(* Don't try to instantiate if a sort because if evar_concl is an
            evar it may commit to a univ level which is not the right
@@ -623,7 +623,7 @@ let rec do_projection_effects define_fun env ty evd = function
            unif, we know that no coercion can be inserted) *)
 	let subst = make_pure_subst evi argsv in
 	let ty' = replace_vars subst evi.evar_concl in
-	let ty' = whd_evar (evars_of evd) ty' in
+	let ty' = whd_evar ( evd) ty' in
 	if isEvar ty' then define_fun env (destEvar ty') ty evd else evd
       else
 	evd
@@ -682,7 +682,7 @@ let effective_projections =
   map_succeed (function Invertible c -> c | _ -> failwith"")
 
 let instance_of_projection f env t evd projs =
-  let ty = lazy (Retyping.get_type_of env (evars_of evd) t) in
+  let ty = lazy (Retyping.get_type_of env ( evd) t) in
   match projs with
   | NoUniqueProjection -> raise NotUnique
   | UniqueProjection (c,effects) ->
@@ -719,7 +719,7 @@ let do_restrict_hyps_virtual evd evk filter =
        interest for this early detection in practice is not obvious. We let
        it for future work. In any case, thanks to the use of filters, the whole
        (unrestricted) context remains consistent. *)
-    let evi = Evd.find (evars_of evd) evk in
+    let evi = Evd.find ( evd) evk in
     let env = evar_unfiltered_env evi in
     let oldfilter = evar_filter evi in
     let filter,_ = List.fold_right (fun oldb (l,filter) ->
@@ -734,7 +734,7 @@ let do_restrict_hyps evd evk projs =
     evd,evk
   else
     let evd,nc = do_restrict_hyps_virtual evd evk filter in
-    let evd = Evd.evar_define evk nc evd in
+    let evd = Evd.define evk nc evd in
     let evk',_ = destEvar nc in
     evd,evk'
 
@@ -742,7 +742,7 @@ let do_restrict_hyps evd evk projs =
 
 let postpone_evar_term env evd (evk,argsv) rhs =
   let rhs = expand_vars_in_term env rhs in
-  let evi = Evd.find (evars_of evd) evk in
+  let evi = Evd.find ( evd) evk in
   let evd,evk,args =
     restrict_upon_filter evd evi evk
       (* Keep only variables that depends in rhs *)
@@ -789,14 +789,14 @@ let postpone_evar_evar env evd projs1 (evk1,args1) projs2 (evk2,args2) =
 exception CannotProject of projectibility_status list
 
 let solve_evar_evar_l2r f env evd (evk1,args1) (evk2,_ as ev2) =
-  let proj1 = array_map_to_list (invert_arg env 0 (evars_of evd) ev2) args1 in
+  let proj1 = array_map_to_list (invert_arg env 0 ( evd) ev2) args1 in
   try
     (* Instantiate ev2 with (a restriction of) ev1 if uniquely projectable *)
     let proj1' = effective_projections proj1 in
     let evd,args1' =
       list_fold_map (instance_of_projection f env (mkEvar ev2)) evd proj1' in
     let evd,evk1' = do_restrict_hyps evd evk1 proj1 in
-    Evd.evar_define evk2 (mkEvar(evk1',Array.of_list args1')) evd
+    Evd.define evk2 (mkEvar(evk1',Array.of_list args1')) evd
   with NotUnique ->
     raise (CannotProject proj1)
 
@@ -842,16 +842,16 @@ exception NotEnoughInformationToProgress
 let rec invert_definition env evd (evk,argsv as ev) rhs =
   let evdref = ref evd in
   let progress = ref false in
-  let evi = Evd.find (evars_of evd) evk in
-  let subst = make_projectable_subst (evars_of evd) evi argsv in
+  let evi = Evd.find ( evd) evk in
+  let subst = make_projectable_subst ( evd) evi argsv in
 
   (* Projection *)
   let project_variable t =
     (* Evar/Var problem: unifiable iff variable projectable from ev subst *)
     try 
-      let sols = find_projectable_vars true env (evars_of !evdref) t subst in
+      let sols = find_projectable_vars true env ( !evdref) t subst in
       let c, p = filter_solution sols in
-      let ty = lazy (Retyping.get_type_of env (evars_of !evdref) t) in
+      let ty = lazy (Retyping.get_type_of env ( !evdref) t) in
       let evd = do_projection_effects evar_define env ty !evdref p in
       evdref := evd;
       c
@@ -871,16 +871,16 @@ let rec invert_definition env evd (evk,argsv as ev) rhs =
 	  evar in
 
   let rec imitate (env',k as envk) t =
-    let t = whd_evar (evars_of !evdref) t in
+    let t = whd_evar ( !evdref) t in
     match kind_of_term t with
     | Rel i when i>k -> project_variable (mkRel (i-k))
     | Var id -> project_variable t
     | Evar (evk',args' as ev') ->
-        if evk = evk' then error_occur_check env (evars_of evd) evk rhs;
+        if evk = evk' then error_occur_check env ( evd) evk rhs;
 	(* Evar/Evar problem (but left evar is virtual) *)
 	let projs' =
 	  array_map_to_list
-	    (invert_arg_from_subst env k (evars_of !evdref) subst) args'
+	    (invert_arg_from_subst env k ( !evdref) subst) args'
 	in
 	(try
 	  (* Try to project (a restriction of) the right evar *)
@@ -909,13 +909,13 @@ let rec invert_definition env evd (evk,argsv as ev) rhs =
 	map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
 	  imitate envk t in
 
-  let rhs = whd_beta (evars_of evd) rhs (* heuristic *) in
+  let rhs = whd_beta ( evd) rhs (* heuristic *) in
   let body = imitate (env,0) rhs in
   (!evdref,body)
 
-(* [evar_define] tries to solve the problem "?ev[args] = rhs" when "?ev" is
+(* [define] tries to solve the problem "?ev[args] = rhs" when "?ev" is
  * an (uninstantiated) evar such that "hyps |- ?ev : typ". Otherwise said,
- * [evar_define] tries to find an instance lhs such that
+ * [define] tries to find an instance lhs such that
  * "lhs [hyps:=args]" unifies to rhs. The term "lhs" must be closed in
  * context "hyps" and not referring to itself.
  *)
@@ -932,7 +932,7 @@ and evar_define env (evk,_ as ev) rhs evd =
     if occur_meta body then error "Meta cannot occur in evar body.";
     (* invert_definition may have instantiate some evars of rhs with evk *)
     (* so we recheck acyclicity *)
-    if occur_evar evk body then error_occur_check env (evars_of evd) evk body;
+    if occur_evar evk body then error_occur_check env ( evd) evk body;
     (* needed only if an inferred type *)
     let body = refresh_universes body in
 (* Cannot strictly type instantiations since the unification algorithm
@@ -943,7 +943,7 @@ and evar_define env (evk,_ as ev) rhs evd =
       try
         let env = evar_env evi in
         let ty = evi.evar_concl in
-        Typing.check env (evars_of evd') body ty
+        Typing.check env ( evd') body ty
       with e ->
         pperrnl
           (str "Ill-typed evar instantiation: " ++ fnl() ++
@@ -951,19 +951,19 @@ and evar_define env (evk,_ as ev) rhs evd =
            str "----> " ++ int ev ++ str " := " ++
            print_constr body);
         raise e in*)
-    Evd.evar_define evk body evd'
+    Evd.define evk body evd'
   with
     | NotEnoughInformationToProgress ->
 	postpone_evar_term env evd ev rhs
     | NotInvertibleUsingOurAlgorithm t -> 
-	error_not_clean env (evars_of evd) evk t (evar_source evk evd)
+	error_not_clean env ( evd) evk t (evar_source evk evd)
 
 (*-------------------*)
 (* Auxiliary functions for the conversion algorithms modulo evars
  *)
 
 let has_undefined_evars evd t =
-  let evm = evars_of evd in
+  let evm =  evd in
   let rec has_ev t =
     match kind_of_term t with
         Evar (ev,args) ->
@@ -1079,7 +1079,7 @@ let solve_pattern_eqn env l1 c =
  * hyps of the existential, to do a "pop" for each Rel which is
  * not an argument of the existential, and a subst1 for each which
  * is, again, with the corresponding variable. This is done by
- * evar_define
+ * define
  *
  * Thus, we take the arguments of the existential which we are about
  * to assign, and zip them with the identifiers in the hypotheses.
@@ -1105,7 +1105,7 @@ let status_changed lev (pbty,_,t1,t2) =
 
 let solve_refl conv_algo env evd evk argsv1 argsv2 =
   if argsv1 = argsv2 then evd else
-  let evi = Evd.find (evars_of evd) evk in
+  let evi = Evd.find ( evd) evk in
   (* Filter and restrict if needed *)
   let evd,evk,args =
     restrict_upon_filter evd evi evk
@@ -1125,7 +1125,7 @@ let solve_refl conv_algo env evd evk argsv1 argsv2 =
 (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *)
 let solve_simple_eqn conv_algo env evd (pbty,(evk1,args1 as ev1),t2) =
   try
-    let t2 = whd_evar (evars_of evd) t2 in
+    let t2 = whd_evar ( evd) t2 in
     let evd = match kind_of_term t2 with
       | Evar (evk2,args2 as ev2) ->
 	  if evk1 = evk2 then
@@ -1136,7 +1136,7 @@ let solve_simple_eqn conv_algo env evd (pbty,(evk1,args1 as ev1),t2) =
 	    else add_conv_pb (pbty,env,mkEvar ev1,t2) evd
       | _ ->
 	  let evd = evar_define env ev1 t2 evd in
-	  let evm = evars_of evd in
+	  let evm =  evd in
 	  let evi = Evd.find evm evk1 in
 	    if occur_existential evm evi.evar_concl then
 	      let evenv = evar_env evi in
@@ -1180,7 +1180,7 @@ let evars_of_evar_info evi =
 (* it assumes that the defined existentials have already been substituted *)
 
 let check_evars env initial_sigma evd c =
-  let sigma = evars_of evd in
+  let sigma =  evd in
   let c = nf_evar sigma c in
   let rec proc_rec c =
     match kind_of_term c with
@@ -1238,7 +1238,7 @@ let mk_valcon c = Some c
    cumulativity now includes Prop and Set in Type...
    It is, but that's not too bad *)
 let define_evar_as_abstraction abs evd (ev,args) =
-  let evi = Evd.find (evars_of evd) ev in
+  let evi = Evd.find ( evd) ev in
   let evenv = evar_unfiltered_env evi in
   let (evd1,dom) = new_evar evd evenv (new_Type()) ~filter:(evar_filter evi) in
   let nvar =
@@ -1249,7 +1249,7 @@ let define_evar_as_abstraction abs evd (ev,args) =
     new_evar evd1 newenv ~src:(evar_source ev evd1) (new_Type()) 
       ~filter:(true::evar_filter evi) in
   let prod = abs (Name nvar, dom, subst_var nvar rng) in
-  let evd3 = Evd.evar_define ev prod evd2 in
+  let evd3 = Evd.define ev prod evd2 in
   let evdom = fst (destEvar dom), args in
   let evrng =
     fst (destEvar rng), array_cons (mkRel 1) (Array.map (lift 1) args) in
@@ -1264,7 +1264,7 @@ let define_evar_as_lambda evd (ev,args) =
 
 let define_evar_as_sort evd (ev,args) =
   let s = new_Type () in
-  Evd.evar_define ev s evd, destSort s
+  Evd.define ev s evd, destSort s
 
 
 (* We don't try to guess in which sort the type should be defined, since
@@ -1279,7 +1279,7 @@ let judge_of_new_Type () = Typeops.judge_of_type (new_univ ())
 
 let split_tycon loc env evd tycon = 
   let rec real_split c = 
-    let sigma = evars_of evd in
+    let sigma =  evd in
     let t = whd_betadeltaiota env sigma c in
       match kind_of_term t with
 	| Prod (na,dom,rng) -> evd, (na, dom, rng)
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 400ad2f7a8..9ee34b40d8 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -23,6 +23,9 @@ open Mod_subst
 
 type evar = existential_key
 
+let string_of_existential evk = "?" ^ string_of_int evk
+let existential_of_int evk = evk
+
 type evar_body =
   | Evar_empty 
   | Evar_defined of constr
@@ -60,97 +63,107 @@ let eq_evar_info ei1 ei2 =
     eq_named_context_val (ei1.evar_hyps) (ei2.evar_hyps) &&
     ei1.evar_body = ei2.evar_body
 
-module Evarmap = Intmap
-
-type evar_map1 = evar_info Evarmap.t
-
-let empty = Evarmap.empty
-
-let to_list evc = (* Workaround for change in Map.fold behavior *)
-  let l = ref [] in 
-  Evarmap.iter (fun evk x -> l := (evk,x)::!l) evc;
-  !l
-
-let dom evc = Evarmap.fold (fun evk _ acc -> evk::acc) evc []
-let find evc k = Evarmap.find k evc
-let remove evc k = Evarmap.remove k evc
-let mem evc k = Evarmap.mem k evc
-let fold = Evarmap.fold
-
-let add evd evk newinfo =  Evarmap.add evk newinfo evd
-
-let define evd evk body = 
-  let oldinfo =
-    try find evd evk
-    with Not_found -> error "Evd.define: cannot define undeclared evar" in
-  let newinfo =
-    { oldinfo with
-      evar_body = Evar_defined body } in
-  match oldinfo.evar_body with
-    | Evar_empty -> Evarmap.add evk newinfo evd
-    | _ -> anomaly "Evd.define: cannot define an evar twice"
-
-let is_evar sigma evk = mem sigma evk
-
-let is_defined sigma evk =
-  let info = find sigma evk in 
-  not (info.evar_body = Evar_empty)
-
-let string_of_existential evk = "?" ^ string_of_int evk
-
-let existential_of_int evk = evk
-
-(*******************************************************************)
-(* Formerly Instantiate module *)
-
-let is_id_inst inst =
-  let is_id (id,c) = match kind_of_term c with
-    | Var id' -> id = id'
-    | _ -> false
-  in
-  List.for_all is_id inst
-
-(* Vérifier que les instances des let-in sont compatibles ?? *)
-let instantiate_sign_including_let sign args =
-  let rec instrec = function
-    | ((id,b,_) :: sign, c::args) -> (id,c) :: (instrec (sign,args))
-    | ([],[])                        -> []
-    | ([],_) | (_,[]) ->
-    anomaly "Signature and its instance do not match"
-  in 
-  instrec (sign,args)
-
-let instantiate_evar sign c args =
-  let inst = instantiate_sign_including_let sign args in
-  if is_id_inst inst then
-    c
-  else
-    replace_vars inst c
-
-(* Existentials. *)
+(* spiwack: Revised hierarchy :
+      - ExistentialMap ( Maps of existential_keys )
+      - EvarInfoMap ( .t = evar_info ExistentialMap.t )
+      - EvarMap ( .t = EvarInfoMap.t * sort_constraints )
+      - evar_defs (exported)
+*)
 
-let existential_type sigma (n,args) =
-  let info =
-    try find sigma n
-    with Not_found ->
-      anomaly ("Evar "^(string_of_existential n)^" was not declared") in
-  let hyps = evar_filtered_context info in
-  instantiate_evar hyps info.evar_concl (Array.to_list args)
+module ExistentialMap = Intmap
 
+(* This exception is raised by *.existential_value *)	
 exception NotInstantiatedEvar
 
-let existential_value sigma (n,args) =
-  let info = find sigma n in
-  let hyps = evar_filtered_context info in
-  match evar_body info with
-    | Evar_defined c ->
-	instantiate_evar hyps c (Array.to_list args)
-    | Evar_empty ->
-	raise NotInstantiatedEvar
+module EvarInfoMap = struct
+  type t = evar_info ExistentialMap.t
+
+  let empty = ExistentialMap.empty
+
+  let to_list evc = (* Workaround for change in Map.fold behavior *)
+    let l = ref [] in 
+    ExistentialMap.iter (fun evk x -> l := (evk,x)::!l) evc;
+    !l
+
+  let dom evc = ExistentialMap.fold (fun evk _ acc -> evk::acc) evc []
+  let find evc k = ExistentialMap.find k evc
+  let remove evc k = ExistentialMap.remove k evc
+  let mem evc k = ExistentialMap.mem k evc
+  let fold = ExistentialMap.fold
+
+  let add evd evk newinfo =  ExistentialMap.add evk newinfo evd
+
+  let equal = ExistentialMap.equal
+
+  let define evd evk body = 
+    let oldinfo =
+      try find evd evk
+      with Not_found -> error "Evd.define: cannot define undeclared evar" in
+    let newinfo =
+      { oldinfo with
+	  evar_body = Evar_defined body } in
+      match oldinfo.evar_body with
+	| Evar_empty -> ExistentialMap.add evk newinfo evd
+	| _ -> anomaly "Evd.define: cannot define an evar twice"
+
+  let is_evar sigma evk = mem sigma evk
+
+  let is_defined sigma evk =
+    let info = find sigma evk in 
+      not (info.evar_body = Evar_empty)
+
+
+  (*******************************************************************)
+  (* Formerly Instantiate module *)
+
+  let is_id_inst inst =
+    let is_id (id,c) = match kind_of_term c with
+      | Var id' -> id = id'
+      | _ -> false
+    in
+      List.for_all is_id inst
+
+  (* Vérifier que les instances des let-in sont compatibles ?? *)
+  let instantiate_sign_including_let sign args =
+    let rec instrec = function
+      | ((id,b,_) :: sign, c::args) -> (id,c) :: (instrec (sign,args))
+      | ([],[])                        -> []
+      | ([],_) | (_,[]) ->
+	  anomaly "Signature and its instance do not match"
+    in 
+      instrec (sign,args)
+
+  let instantiate_evar sign c args =
+    let inst = instantiate_sign_including_let sign args in
+      if is_id_inst inst then
+	c
+      else
+	replace_vars inst c
+
+  (* Existentials. *)
+
+  let existential_type sigma (n,args) =
+    let info =
+      try find sigma n
+      with Not_found ->
+	anomaly ("Evar "^(string_of_existential n)^" was not declared") in
+    let hyps = evar_filtered_context info in
+      instantiate_evar hyps info.evar_concl (Array.to_list args)
+
+  let existential_value sigma (n,args) =
+    let info = find sigma n in
+    let hyps = evar_filtered_context info in
+      match evar_body info with
+	| Evar_defined c ->
+	    instantiate_evar hyps c (Array.to_list args)
+	| Evar_empty ->
+	    raise NotInstantiatedEvar
+
+  let existential_opt_value sigma ev =
+    try Some (existential_value sigma ev)
+    with NotInstantiatedEvar -> None
 
-let existential_opt_value sigma ev =
-  try Some (existential_value sigma ev)
-  with NotInstantiatedEvar -> None
+end
 
 (*******************************************************************)
 (*                Constraints for sort variables                   *)
@@ -285,39 +298,29 @@ let pr_sort_cstrs g =
           hov 0 (prlist_with_sep spc Univ.pr_uni leq) ++ str"]")
     l
 
-type evar_map = evar_map1 * sort_constraints
-let empty = empty, UniverseMap.empty
-let add (sigma,sm) k v = (add sigma k v, sm)
-let dom (sigma,_) = dom sigma
-let find (sigma,_) = find sigma
-let remove (sigma,sm) k = (remove sigma k, sm)
-let mem (sigma,_) = mem sigma
-let to_list (sigma,_) = to_list sigma
-let fold f (sigma,_) = fold f sigma
-let define (sigma,sm) k v = (define sigma k v, sm)
-let is_evar (sigma,_) = is_evar sigma
-let is_defined (sigma,_) = is_defined sigma
-let existential_value (sigma,_) = existential_value sigma
-let existential_type (sigma,_) = existential_type sigma
-let existential_opt_value (sigma,_) = existential_opt_value sigma
-let eq_evar_map x y = x == y ||
-  (Evarmap.equal eq_evar_info (fst x) (fst y) &&
+module EvarMap = struct
+  type t = EvarInfoMap.t * sort_constraints
+  let empty = EvarInfoMap.empty, UniverseMap.empty
+  let add (sigma,sm) k v = (EvarInfoMap.add sigma k v, sm)
+  let dom (sigma,_) = EvarInfoMap.dom sigma
+  let find (sigma,_) = EvarInfoMap.find sigma
+  let remove (sigma,sm) k = (EvarInfoMap.remove sigma k, sm)
+  let mem (sigma,_) = EvarInfoMap.mem sigma
+  let to_list (sigma,_) = EvarInfoMap.to_list sigma
+  let fold f (sigma,_) = EvarInfoMap.fold f sigma
+  let define (sigma,sm) k v = (EvarInfoMap.define sigma k v, sm)
+  let is_evar (sigma,_) = EvarInfoMap.is_evar sigma
+  let is_defined (sigma,_) = EvarInfoMap.is_defined sigma
+  let existential_value (sigma,_) = EvarInfoMap.existential_value sigma
+  let existential_type (sigma,_) = EvarInfoMap.existential_type sigma
+  let existential_opt_value (sigma,_) = EvarInfoMap.existential_opt_value sigma
+  let eq_evar_map x y = x == y ||
+    (EvarInfoMap.equal eq_evar_info (fst x) (fst y) &&
       UniverseMap.equal (=) (snd x) (snd y))
 
-let merge e e' = fold (fun n v sigma -> add sigma n v) e' e
-
-(*******************************************************************)
-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_map}
- 
-let sig_it x = x.it
-let sig_sig x = x.sigma
+  let merge e e' = fold (fun n v sigma -> add sigma n v) e' e
+  
+end
  
 (*******************************************************************)
 (* Metamaps *)
@@ -418,12 +421,55 @@ type hole_kind =
 type conv_pb = Reduction.conv_pb
 type evar_constraint = conv_pb * Environ.env * constr * constr
 type evar_defs =
-    { evars : evar_map;
+    { evars : EvarMap.t;
       conv_pbs : evar_constraint list;
       last_mods : existential_key list;
       history : (existential_key * (loc * hole_kind)) list;
       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 *)
+let merge d1 d2 = {
+(* d1 with evars = EvarMap.merge d1.evars d2.evars*)
+  evars = EvarMap.merge d1.evars d2.evars ;
+  conv_pbs = List.rev_append d1.conv_pbs d2.conv_pbs ;
+  last_mods = List.rev_append d1.last_mods d2.last_mods ;
+  history = List.rev_append d1.history d2.history ;
+  metas = Metamap.fold (fun k m r -> Metamap.add k m r) d2.metas d1.metas
+}
+let add d e i = { d with evars=EvarMap.add d.evars e i }
+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
+   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 
+    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
+let is_defined d e = EvarMap.is_defined d.evars e
+
+let existential_value d e = EvarMap.existential_value d.evars e
+let existential_type d e = EvarMap.existential_type d.evars e
+let existential_opt_value d e = EvarMap.existential_opt_value d.evars e
+
+(*** /Lifting... ***)
+
+(* evar_defs are considered empty disregarding histories *)
+let is_empty d = 
+  d.evars = EvarMap.empty &&
+  d.conv_pbs = [] &&
+  Metamap.is_empty d.metas
+
 let subst_named_context_val s = map_named_val (subst_mps s)
 
 let subst_evar_info s evi = 
@@ -434,36 +480,40 @@ let subst_evar_info s evi =
       evar_hyps = subst_named_context_val s evi.evar_hyps;
       evar_body = subst_evb evi.evar_body }
 
-let subst_evar_map sub evm = 
-  assert (snd evm = UniverseMap.empty);
-  Evarmap.map (subst_evar_info sub) (fst evm), snd evm
-
 let subst_evar_defs_light sub evd =
-  assert (snd evd.evars = UniverseMap.empty);
+  assert (UniverseMap.is_empty (snd evd.evars));
   assert (evd.conv_pbs = []);
   { evd with
       metas = Metamap.map (map_clb (subst_mps sub)) evd.metas;
-      evars = Evarmap.map (subst_evar_info sub)  (fst evd.evars), snd evd.evars
+      evars = ExistentialMap.map (subst_evar_info sub)  (fst evd.evars), snd evd.evars
   }
 
-let create_evar_defs sigma =
-  { evars=sigma; conv_pbs=[]; last_mods = []; history=[]; metas=Metamap.empty }
-let create_goal_evar_defs sigma =
-  let h = fold (fun mv _ l -> (mv,(dummy_loc,GoalEvar))::l) sigma [] in
-  { evars=sigma; conv_pbs=[]; last_mods = []; history=h; metas=Metamap.empty }
-let empty_evar_defs = create_evar_defs empty
-let evars_of d = d.evars
-let evars_reset_evd evd d = {d with evars = evd}
-let reset_evd (sigma,mmap) d = {d with evars = sigma; metas=mmap}
+let subst_evar_map = subst_evar_defs_light
+
+(* spiwack: deprecated *)
+let create_evar_defs sigma = { sigma with
+  conv_pbs=[]; last_mods=[]; history=[]; metas=Metamap.empty }
+(* spiwack: tentatively deprecated *)
+let create_goal_evar_defs sigma = { sigma with
+   conv_pbs=[]; last_mods=[]; metas=Metamap.empty }
+let empty =  { 
+  evars=EvarMap.empty; 
+  conv_pbs=[]; 
+  last_mods = []; 
+  history=[]; 
+  metas=Metamap.empty 
+}
+
+let evars_reset_evd evd d = {d with evars = evd.evars}
 let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs}
 let evar_source evk d =
   try List.assoc evk d.history
   with Not_found -> (dummy_loc, InternalHole)
 
 (* define the existential of section path sp as the constr body *)
-let evar_define evk body evd =
+let define evk body evd =
   { evd with
-    evars = define evd.evars evk body;
+    evars = EvarMap.define evd.evars evk body;
     last_mods = evk :: evd.last_mods }
 
 let evar_declare hyps evk ty ?(src=(dummy_loc,InternalHole)) ?filter evd =
@@ -476,7 +526,7 @@ let evar_declare hyps evk ty ?(src=(dummy_loc,InternalHole)) ?filter evd =
       filter)
   in
   { evd with
-    evars = add evd.evars evk
+    evars = EvarMap.add evd.evars evk
       {evar_hyps = hyps;
        evar_concl = ty;
        evar_body = Evar_empty;
@@ -484,7 +534,7 @@ let evar_declare hyps evk ty ?(src=(dummy_loc,InternalHole)) ?filter evd =
        evar_extra = None};
     history = (evk,src)::evd.history }
 
-let is_defined_evar evd (evk,_) = is_defined evd.evars evk
+let is_defined_evar evd (evk,_) = EvarMap.is_defined evd.evars evk
 
 (* Does k corresponds to an (un)defined existential ? *)
 let is_undefined_evar evd c = match kind_of_term c with
@@ -493,9 +543,9 @@ let is_undefined_evar evd c = match kind_of_term c with
 
 let undefined_evars evd = 
   let evars = 
-    fold (fun evk evi sigma -> if evi.evar_body = Evar_empty then 
-	    add sigma evk evi else sigma) 
-      evd.evars empty
+    EvarMap.fold (fun evk evi sigma -> if evi.evar_body = Evar_empty then 
+	    EvarMap.add sigma evk evi else sigma) 
+      evd.evars EvarMap.empty
   in 
     { evd with evars = evars }
 
@@ -521,23 +571,24 @@ let extract_changed_conv_pbs evd p =
 let extract_all_conv_pbs evd =
   extract_conv_pbs evd (fun _ -> true)
 
+(* spiwack: should it be replaced by Evd.merge? *)
 let evar_merge evd evars =
-  { evd with evars = merge evd.evars evars }
+  { evd with evars = EvarMap.merge evd.evars evars.evars }
 
 (**********************************************************)
 (* Sort variables *)
 
-let new_sort_variable (sigma,sm) =
+let new_sort_variable ({ evars = (sigma,sm) } as d)=
   let (u,scstr) = new_sort_var sm in
-  (Type u,(sigma,scstr))
-let is_sort_variable (_,sm) s =
+  (Type u,{ d with evars = (sigma,scstr) } )
+let is_sort_variable {evars=(_,sm)} s =
   is_sort_var s sm
-let whd_sort_variable (_,sm) t = whd_sort_var sm t
-let set_leq_sort_variable (sigma,sm) u1 u2 =
-  (sigma, set_leq u1 u2 sm)
-let define_sort_variable (sigma,sm) u s =
-  (sigma, set_sort_variable u s sm)
-let pr_sort_constraints (_,sm) = pr_sort_cstrs sm
+let whd_sort_variable {evars=(_,sm)} t = whd_sort_var sm t
+let set_leq_sort_variable ({evars=(sigma,sm)}as d) u1 u2 =
+  { d with evars = (sigma, set_leq u1 u2 sm) }
+let define_sort_variable ({evars=(sigma,sm)}as d) u s =
+  { d with evars = (sigma, set_sort_variable u s sm) }
+let pr_sort_constraints {evars=(_,sm)} = pr_sort_cstrs sm
 
 (**********************************************************)
 (* Accessing metas *)
@@ -630,6 +681,7 @@ let meta_with_name evd id =
            strbrk "\" occurs more than once in clause.")
 
 
+(* spiwack: we should try and replace this List.fold_left by a Metamap.fold.  *)
 let meta_merge evd1 evd2 =
   {evd2 with
     metas = List.fold_left (fun m (n,v) -> Metamap.add n v m) 
@@ -658,6 +710,19 @@ let subst_defined_metas bl c =
     | _ -> map_constr substrec c
   in try Some (substrec c) with Not_found -> None
 
+(*******************************************************************)
+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_map}
+ 
+let sig_it x = x.it
+let sig_sig x = x.sigma
+
 (**********************************************************)
 (* Failure explanation *)
 
@@ -713,12 +778,12 @@ let pr_evar_info evi =
   in
   hov 2 (str"["  ++ phyps ++ spc () ++ str"|- "  ++ pty ++ pb ++ str"]")
 
-let pr_evar_map sigma =
+let pr_evar_defs_t sigma =
   h 0 
     (prlist_with_sep pr_fnl
       (fun (ev,evi) ->
         h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi))
-      (to_list sigma))
+      (EvarMap.to_list sigma))
 
 let pr_constraints pbs =
   h 0
@@ -731,8 +796,8 @@ let pr_constraints pbs =
 
 let pr_evar_defs evd =
   let pp_evm =
-    if evd.evars = empty then mt() else
-      str"EVARS:"++brk(0,1)++pr_evar_map evd.evars++fnl() in
+    if evd.evars = EvarMap.empty then mt() else
+      str"EVARS:"++brk(0,1)++pr_evar_defs_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 6694e63dda..8ea0227fed 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -20,84 +20,6 @@ open Mod_subst
 open Termops
 (*i*)
 
-(* The type of mappings for existential variables.
-   The keys are integers and the associated information is a record
-   containing the type of the evar ([evar_concl]), the context under which 
-   it was introduced ([evar_hyps]) and its definition ([evar_body]). 
-   [evar_info] is used to add any other kind of information. *)
-
-type evar = existential_key
-
-type evar_body =
-  | Evar_empty 
-  | Evar_defined of constr
-
-type evar_info = {
-  evar_concl : constr;
-  evar_hyps : named_context_val;
-  evar_body : evar_body;
-  evar_filter : bool list;
-  evar_extra : Dyn.t option}
-
-val eq_evar_info : evar_info -> evar_info -> bool
-
-val make_evar : named_context_val -> types -> evar_info
-val evar_concl : evar_info -> constr
-val evar_context : evar_info -> named_context
-val evar_filtered_context : evar_info -> named_context
-val evar_hyps : evar_info -> named_context_val
-val evar_body : evar_info -> evar_body
-val evar_filter : evar_info -> bool list
-val evar_unfiltered_env :  evar_info -> env
-val evar_env :  evar_info -> env
-
-type evar_map
-val eq_evar_map : evar_map -> evar_map -> bool
-
-val empty : evar_map
-
-val add : evar_map -> evar -> evar_info -> evar_map
-
-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_map -> evar_map -> evar_map
-
-val define : evar_map -> evar -> constr -> evar_map
-
-val is_evar : evar_map -> evar -> bool
-
-val is_defined : evar_map -> evar -> bool
-
-val string_of_existential : evar -> string
-val existential_of_int : int -> evar
-
-(*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_map -> existential -> constr
-val existential_type : evar_map -> existential -> types
-val existential_opt_value : evar_map -> existential -> constr option
-
-(*********************************************************************)
-(* constr with holes *)
-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_map}
-
-val sig_it  : 'a sigma -> 'a
-val sig_sig : 'a sigma -> evar_map
-
 (*********************************************************************)
 (* Meta map *)
 
@@ -153,20 +75,92 @@ type clbinding =
 
 val map_clb : (constr -> constr) -> clbinding -> clbinding
 
+
 (*********************************************************************)
-(* Unification state *)
+(*** Existential variables and unification states ***)
+
+(* A unification state (of type [evar_defs]) 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 
+   kind of information. 
+   It also contains conversion constraints, debugging information and 
+   information about meta variables. *)
+
+(* Information about existential variables. *)
+type evar = existential_key
+
+val string_of_existential : evar -> string
+val existential_of_int : int -> evar
+
+type evar_body =
+  | Evar_empty 
+  | Evar_defined of constr
+
+type evar_info = {
+  evar_concl : constr;
+  evar_hyps : named_context_val;
+  evar_body : evar_body;
+  evar_filter : bool list;
+  evar_extra : Dyn.t option}
+
+val eq_evar_info : evar_info -> evar_info -> bool
+
+val make_evar : named_context_val -> types -> evar_info
+val evar_concl : evar_info -> constr
+val evar_context : evar_info -> named_context
+val evar_filtered_context : evar_info -> named_context
+val evar_hyps : evar_info -> named_context_val
+val evar_body : evar_info -> evar_body
+val evar_filter : evar_info -> bool list
+val evar_unfiltered_env :  evar_info -> env
+val evar_env :  evar_info -> env
+
+(*** Unification state ***)
 type evar_defs
 
-val subst_evar_map : substitution -> evar_map -> 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 empty : evar_defs
+val is_empty : evar_defs -> bool
+
+val add : evar_defs -> evar -> evar_info -> evar_defs
+
+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 merge : evar_defs -> evar_defs -> evar_defs
+
+val define : evar -> constr -> evar_defs -> evar_defs
+
+val is_evar : evar_defs -> evar -> bool
+
+val is_defined : evar_defs -> 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
+
 (* Assume empty universe constraints in [evar_map] and [conv_pbs] *)
 val subst_evar_defs_light : substitution -> evar_defs -> evar_defs
 
-(* create an [evar_defs] with empty meta map: *)
-val create_evar_defs      : evar_map -> evar_defs
-val create_goal_evar_defs : evar_map -> evar_defs
-val empty_evar_defs : evar_defs
-val evars_of         : evar_defs -> evar_map
-val evars_reset_evd  : evar_map ->  evar_defs -> evar_defs
+(* spiwack: this function seems to somewhat break the abstraction. *)
+val evars_reset_evd  : evar_defs ->  evar_defs -> evar_defs
+
+
+
 
 (* Should the obligation be defined (opaque or transparent (default)) or
    defined transparent and expanded in the term? *)
@@ -183,17 +177,19 @@ type hole_kind =
   | TomatchTypeParameter of inductive * int
   | GoalEvar
   | ImpossibleCase
-val is_defined_evar :  evar_defs -> existential -> bool
+
+(* 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 evar_declare :
   named_context_val -> evar -> types -> ?src:loc * hole_kind ->
       ?filter:bool list -> evar_defs -> evar_defs
-val evar_define : evar -> constr -> evar_defs -> evar_defs
 val evar_source : existential_key -> evar_defs -> loc * hole_kind
 
+(* spiwack: this function seesm to somewhat break the abstraction. *)
 (* [evar_merge evd evars] extends the evars of [evd] with [evars] *)
-val evar_merge : evar_defs -> evar_map -> evar_defs
+val evar_merge : evar_defs -> evar_defs -> evar_defs
 
 (* Unification constraints *)
 type conv_pb = Reduction.conv_pb
@@ -236,11 +232,25 @@ val subst_defined_metas : metabinding list -> constr -> constr option
 (**********************************************************)
 (* Sort variables *)
 
-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
+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
+
+(*********************************************************************)
+(* constr with holes *)
+type open_constr = evar_defs * constr
+
+(*********************************************************************)
+(* The type constructor ['a sigma] adds an evar map to an object of
+  type ['a] *)
+type 'a sigma = {
+  it : 'a ;
+  sigma : evar_defs}
+
+val sig_it  : 'a sigma -> 'a
+val sig_sig : 'a sigma -> evar_defs
 
 (**********************************************************)
 (* Failure explanation *)
@@ -251,7 +261,16 @@ type unsolvability_explanation = SeveralInstancesFound of int
 (* debug pretty-printer: *)
 
 val pr_evar_info : evar_info -> Pp.std_ppcmds
-val pr_evar_map  : evar_map -> Pp.std_ppcmds
 val pr_evar_defs : evar_defs -> Pp.std_ppcmds
-val pr_sort_constraints : evar_map -> Pp.std_ppcmds
+val pr_sort_constraints : evar_defs -> 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
+(*** /Deprecaded ***)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 35c5d376ba..0fd2fccb4a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -204,14 +204,14 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	for i = 0 to lt-1 do 
           if not (e_cumul env evdref (vdefj.(i)).uj_type
 		    (lift lt lar.(i))) then
-            error_ill_typed_rec_body_loc loc env (evars_of !evdref)
+            error_ill_typed_rec_body_loc loc env ( !evdref)
               i lna vdefj lar
 	done
 
   let check_branches_message loc env evdref c (explft,lft) = 
     for i = 0 to Array.length explft - 1 do
       if not (e_cumul env evdref lft.(i) explft.(i)) then 
-	let sigma = evars_of !evdref in
+	let sigma =  !evdref in
 	  error_ill_formed_branch_loc loc env sigma c i lft.(i) explft.(i)
     done
 
@@ -267,7 +267,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
       {uj_val=it_mkLambda ccl' sign; uj_type=it_mkProd s' sign} 
 
   let evar_kind_of_term sigma c =
-    kind_of_term (whd_evar (Evd.evars_of sigma) c)
+    kind_of_term (whd_evar ( sigma) c)
 
   (*************************************************************************)
   (* Main pretyping function                                               *)
@@ -299,12 +299,12 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     | REvar (loc, evk, instopt) ->
 	(* Ne faudrait-il pas s'assurer que hyps est bien un
 	   sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
-	let hyps = evar_filtered_context (Evd.find (evars_of !evdref) evk) in
+	let hyps = evar_filtered_context (Evd.find ( !evdref) evk) in
 	let args = match instopt with
           | None -> instance_from_named_context hyps
           | Some inst -> failwith "Evar subtitutions not implemented" in
 	let c = mkEvar (evk, args) in
-	let j = (Retyping.get_judgment_of env (evars_of !evdref) c) in
+	let j = (Retyping.get_judgment_of env ( !evdref) c) in
 	  inh_conv_coerce_to_tycon loc env evdref j tycon
 
     | RPatVar (loc,(someta,n)) -> 
@@ -356,8 +356,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		   uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
             ctxtv vdef in
 	evar_type_fixpoint loc env evdref names ftys vdefj;
-	let ftys = Array.map (nf_evar (evars_of !evdref)) ftys in
-	let fdefs = Array.map (fun x -> nf_evar (evars_of !evdref) (j_val x)) vdefj in
+	let ftys = Array.map (nf_evar ( !evdref)) ftys in
+	let fdefs = Array.map (fun x -> nf_evar ( !evdref) (j_val x)) vdefj in
  	let fixj = match fixkind with
 	  | RFix (vn,i) ->
 	      (* First, let's find the guard indexes. *)
@@ -392,7 +392,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  | c::rest ->
 	      let argloc = loc_of_rawconstr c in
 	      let resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in
-              let resty = whd_betadeltaiota env (evars_of !evdref) resj.uj_type in
+              let resty = whd_betadeltaiota env ( !evdref) resj.uj_type in
       		match kind_of_term resty with
 		  | Prod (na,c1,c2) ->
 		      let hj = pretype (mk_tycon c1) env evdref lvar c in
@@ -404,19 +404,19 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		  | _ ->
 		      let hj = pretype empty_tycon env evdref lvar c in
 			error_cant_apply_not_functional_loc 
-			  (join_loc floc argloc) env (evars_of !evdref)
+			  (join_loc floc argloc) env ( !evdref)
 	      		  resj [hj]
 	in
 	let resj = apply_rec env 1 fj args in
 	let resj =
 	  match evar_kind_of_term !evdref resj.uj_val with
 	  | App (f,args) ->
-              let f = whd_evar (Evd.evars_of !evdref) f in
+              let f = whd_evar ( !evdref) f in
               begin match kind_of_term f with
               | Ind _ | Const _
 		  when isInd f or has_polymorphic_type (destConst f)
 		    ->
-	          let sigma = evars_of !evdref in
+	          let sigma =  !evdref in
 		  let c = mkApp (f,Array.map (whd_evar sigma) args) in
 	          let t = Retyping.get_type_of env sigma c in
 		  make_judge c t
@@ -454,10 +454,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     | RLetTuple (loc,nal,(na,po),c,d) ->
 	let cj = pretype empty_tycon env evdref lvar c in
 	let (IndType (indf,realargs)) = 
-	  try find_rectype env (evars_of !evdref) cj.uj_type
+	  try find_rectype env ( !evdref) cj.uj_type
 	  with Not_found ->
 	    let cloc = loc_of_rawconstr c in
-	      error_case_not_inductive_loc cloc env (evars_of !evdref) cj 
+	      error_case_not_inductive_loc cloc env ( !evdref) cj 
 	in
 	let cstrs = get_constructors env indf in
 	  if Array.length cstrs <> 1 then
@@ -488,7 +488,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		       (Array.to_list cs.cs_concl_realargs)
 		       @[build_dependent_constructor cs] in
 		     let lp = lift cs.cs_nargs p in
-		     let fty = hnf_lam_applist env (evars_of !evdref) lp inst in
+		     let fty = hnf_lam_applist env ( !evdref) lp inst in
 		     let fj = pretype (mk_tycon fty) env_f evdref lvar d in
 		     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
 		     let v =
@@ -506,7 +506,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		       if noccur_between 1 cs.cs_nargs ccl then
 			 lift (- cs.cs_nargs) ccl 
 		       else
-			 error_cant_find_case_type_loc loc env (evars_of !evdref) 
+			 error_cant_find_case_type_loc loc env ( !evdref) 
 			   cj.uj_val in
 		     let ccl = refresh_universes ccl in
 		     let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
@@ -520,10 +520,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     | RIf (loc,c,(na,po),b1,b2) ->
 	let cj = pretype empty_tycon env evdref lvar c in
 	let (IndType (indf,realargs)) = 
-	  try find_rectype env (evars_of !evdref) cj.uj_type
+	  try find_rectype env ( !evdref) cj.uj_type
 	  with Not_found ->
 	    let cloc = loc_of_rawconstr c in
-	      error_case_not_inductive_loc cloc env (evars_of !evdref) cj in
+	      error_case_not_inductive_loc cloc env ( !evdref) cj in
 	let cstrs = get_constructors env indf in 
 	  if Array.length cstrs <> 2 then
             user_err_loc (loc,"",
@@ -542,7 +542,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	    | Some p ->
 		let env_p = push_rels psign env in
 		let pj = pretype_type empty_valcon env_p evdref lvar p in
-		let ccl = nf_evar (evars_of !evdref) pj.utj_val in
+		let ccl = nf_evar ( !evdref) pj.utj_val in
 		let pred = it_mkLambda_or_LetIn ccl psign in
 		let typ = lift (- nar) (beta_applist (pred,[cj.uj_val])) in
 		let jtyp = inh_conv_coerce_to_tycon loc env evdref {uj_val = pred;
@@ -556,8 +556,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
                       e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ())
 		in
 		  it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
-	  let pred = nf_evar (evars_of !evdref) pred in
-	  let p = nf_evar (evars_of !evdref) p in
+	  let pred = nf_evar ( !evdref) pred in
+	  let p = nf_evar ( !evdref) p in
 	  let f cs b =
 	    let n = rel_context_length cs.cs_args in
 	    let pi = lift n pred in (* liftn n 2 pred ? *)
@@ -612,7 +612,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     | RDynamic (loc,d) ->
 	if (tag d) = "constr" then
 	  let c = constr_out d in
-	  let j = (Retyping.get_judgment_of env (evars_of !evdref) c) in
+	  let j = (Retyping.get_judgment_of env ( !evdref) c) in
 	    j
 	      (*inh_conv_coerce_to_tycon loc env evdref j tycon*)
 	else
@@ -624,7 +624,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	(match valcon with
 	   | Some v ->
                let s =
-		 let sigma = evars_of !evdref in
+		 let sigma =  !evdref in
 		 let t = Retyping.get_type_of env sigma v in
 		   match kind_of_term (whd_betadeltaiota env sigma t) with
                      | Sort s -> s
@@ -648,7 +648,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		if e_cumul env evdref v tj.utj_val then tj
 		else
 		  error_unexpected_type_loc
-                    (loc_of_rawconstr c) env (evars_of !evdref) tj.utj_val v
+                    (loc_of_rawconstr c) env ( !evdref) tj.utj_val v
 
   let pretype_gen_aux evdref env lvar kind c =
     let c' = match kind with
@@ -675,15 +675,15 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     let evdref = ref (create_evar_defs sigma) in
     let j = pretype empty_tycon env evdref ([],[]) c in
     let evd,_ = consider_remaining_unif_problems env !evdref in
-    let j = j_nf_evar (evars_of evd) j in
+    let j = j_nf_evar ( evd) j in
     let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env evd in
-    let j = j_nf_evar (evars_of evd) j in
+    let j = j_nf_evar ( evd) j in
     check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
     j
 
   let understand_judgment_tcc evdref env c =
     let j = pretype empty_tycon env evdref ([],[]) c in
-    let sigma = evars_of !evdref in
+    let sigma =  !evdref in
     let j = j_nf_evar sigma j in
     j
 
@@ -727,7 +727,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	else
 	  pretype_gen_aux evdref env ([],[]) (OfType exptyp) c
       in !evdref, c
-    in Evd.evars_of evd, t
+    in  evd, t
 end
   
 module Default : S = Pretyping_F(Coercion.Default)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index cca6b18558..d3bbce9e31 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -376,7 +376,7 @@ exception Partial
    reduction is solved by the expanded fix term. *)
 let solve_arity_problem env sigma fxminargs c =
   let evm = ref sigma in
-  let set_fix i = evm := Evd.define !evm i (mkVar vfx) in
+  let set_fix i = evm := Evd.define i (mkVar vfx) !evm in
   let rec check strict c =
     let c' = whd_betaiotazeta sigma c in
     let (h,rcargs) = decompose_app c' in
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index e6b590b038..38e4fb677c 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -332,7 +332,7 @@ let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false)
 let solve_instanciation_problem = ref (fun _ _ _ -> assert false)
 
 let resolve_typeclasses ?(onlyargs=false) ?(split=true) ?(fail=true) env evd =
-  if not (has_typeclasses (Evd.evars_of evd)) then evd
+  if not (has_typeclasses ( evd)) then evd
   else
     !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) onlyargs split fail
 
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index ba3eae6fa7..fc43628752 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -47,7 +47,7 @@ let unsatisfiable_constraints env evd ev =
     | None ->
 	raise (TypeClassError (env, UnsatisfiableConstraints (evd, None)))
     | Some ev ->
-	let evi = Evd.find (Evd.evars_of evd) ev in
+	let evi = Evd.find ( evd) ev in
 	let loc, kind = Evd.evar_source ev evd in
 	  raise (Stdpp.Exc_located (loc, TypeClassError
 	    (env, UnsatisfiableConstraints (evd, Some (evi, kind)))))
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index ece3586a19..c22a160480 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -43,30 +43,30 @@ let inductive_type_knowing_parameters env ind jl =
 let rec execute env evd cstr =
   match kind_of_term cstr with
     | Meta n ->
-        { uj_val = cstr; uj_type = nf_evar (evars_of evd) (meta_type evd n) }
+        { uj_val = cstr; uj_type = nf_evar ( evd) (meta_type evd n) }
 
     | Evar ev ->
-        let sigma = Evd.evars_of evd in
+        let sigma =  evd in
 	let ty = Evd.existential_type sigma ev in
-	let jty = execute env evd (nf_evar (evars_of evd) ty) in
+	let jty = execute env evd (nf_evar ( evd) ty) in
 	let jty = assumption_of_judgment env jty in
 	{ uj_val = cstr; uj_type = jty }
 	
     | Rel n -> 
-	j_nf_evar (evars_of evd) (judge_of_relative env n)
+	j_nf_evar ( evd) (judge_of_relative env n)
 
     | Var id -> 
-        j_nf_evar (evars_of evd) (judge_of_variable env id)
+        j_nf_evar ( evd) (judge_of_variable env id)
 	  
     | Const c ->
-        make_judge cstr (nf_evar (evars_of evd) (type_of_constant env c))
+        make_judge cstr (nf_evar ( evd) (type_of_constant env c))
 	  
     | Ind ind ->
-	make_judge cstr (nf_evar (evars_of evd) (type_of_inductive env ind))
+	make_judge cstr (nf_evar ( evd) (type_of_inductive env ind))
 	  
     | Construct cstruct -> 
 	make_judge cstr
-          (nf_evar (evars_of evd) (type_of_constructor env cstruct))
+          (nf_evar ( evd) (type_of_constructor env cstruct))
 
     | Case (ci,p,c,lf) ->
         let cj = execute env evd c in
@@ -101,12 +101,12 @@ let rec execute env evd cstr =
 		(* Sort-polymorphism of inductive types *)
 		make_judge f
 		  (inductive_type_knowing_parameters env ind
-		    (jv_nf_evar (evars_of evd) jl))
+		    (jv_nf_evar ( evd) jl))
 	    | Const cst -> 
 		(* Sort-polymorphism of inductive types *)
 		make_judge f
 		  (constant_type_knowing_parameters env cst
-		    (jv_nf_evar (evars_of evd) jl))
+		    (jv_nf_evar ( evd) jl))
 	    | _ -> 
 		execute env evd f
 	in
@@ -157,7 +157,7 @@ and execute_array env evd = Array.map (execute env evd)
 and execute_list env evd = List.map (execute env evd)
 
 let mcheck env evd c t =
-  let sigma = Evd.evars_of evd in
+  let sigma =  evd in
   let j = execute env evd (nf_evar sigma c) in
   if not (is_conv_leq env sigma j.uj_type t) then
     error_actual_type env j (nf_evar sigma t)
@@ -165,13 +165,13 @@ let mcheck env evd c t =
 (* Type of a constr *)
  
 let mtype_of env evd c =
-  let j = execute env evd (nf_evar (evars_of evd) c) in
+  let j = execute env evd (nf_evar ( evd) c) in
   (* We are outside the kernel: we take fresh universes *)
   (* to avoid tactics and co to refresh universes themselves *)
   Termops.refresh_universes j.uj_type
 
 let msort_of env evd c =
-  let j = execute env evd (nf_evar (evars_of evd) c) in
+  let j = execute env evd (nf_evar ( evd) c) in
   let a = type_judgment env j in
   a.utj_type
 
@@ -185,5 +185,5 @@ let check env sigma c   =
 (* The typed type of a judgment. *)
 
 let mtype_of_type env evd constr =
-  let j = execute env evd (nf_evar (evars_of evd) constr) in
+  let j = execute env evd (nf_evar ( evd) constr) in
   assumption_of_judgment env j
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 54421f96f8..4134f89b27 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -43,14 +43,14 @@ let abstract_scheme env c l lname_typ =
     lname_typ
 
 let abstract_list_all env evd typ c l =
-  let ctxt,_ = splay_prod_n env (evars_of evd) (List.length l) typ in
+  let ctxt,_ = splay_prod_n env ( evd) (List.length l) typ in
   let l_with_all_occs = List.map (function a -> (all_occurrences,a)) l in
   let p = abstract_scheme env c l_with_all_occs ctxt in 
   try 
-    if is_conv_leq env (evars_of evd) (Typing.mtype_of env evd p) typ then p
+    if is_conv_leq env ( evd) (Typing.mtype_of env evd p) typ then p
     else error "abstract_list_all"
   with UserError _ | Type_errors.TypeError _ ->
-    error_cannot_find_well_typed_abstraction env (evars_of evd) p l
+    error_cannot_find_well_typed_abstraction env ( evd) p l
 
 (**)
 
@@ -431,14 +431,14 @@ let applyHead env evd n c  =
     if n = 0 then 
       (evd, c)
     else 
-      match kind_of_term (whd_betadeltaiota env (evars_of evd) cty) with
+      match kind_of_term (whd_betadeltaiota env ( evd) cty) with
         | Prod (_,c1,c2) ->
             let (evd',evar) = 
 	      Evarutil.new_evar evd env ~src:(dummy_loc,GoalEvar) c1 in
 	    apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd'
 	| _ -> error "Apply_Head_Then"
   in 
-  apprec n c (Typing.type_of env (evars_of evd) c) evd
+  apprec n c (Typing.type_of env ( evd) c) evd
 
 let is_mimick_head f =
   match kind_of_term f with
@@ -468,7 +468,7 @@ let try_to_coerce env evd c cty tycon =
   let (evd',j') = inh_conv_coerce_rigid_to dummy_loc env evd j tycon in
   let (evd',b) = Evarconv.consider_remaining_unif_problems env evd' in
   if b then
-    let evd' = Evd.map_metas_fvalue (nf_evar (evars_of evd')) evd' in
+    let evd' = Evd.map_metas_fvalue (nf_evar ( evd')) evd' in
     (evd',j'.uj_val)
   else
     error "Cannot solve unification constraints"
@@ -481,16 +481,16 @@ let w_coerce_to_type env evd c cty mvty =
     (* inh_conv_coerce_rigid_to should have reasoned modulo reduction 
        but there are cases where it though it was not rigid (like in
        fst (nat,nat)) and stops while it could have seen that it is rigid *)
-    let cty = Tacred.hnf_constr env (evars_of evd) cty in
+    let cty = Tacred.hnf_constr env ( evd) cty in
     try_to_coerce env evd c cty tycon
 
 let w_coerce env evd mv c =
-  let cty = get_type_of_with_meta env (evars_of evd) (metas_of evd) c in
+  let cty = get_type_of_with_meta env ( evd) (metas_of evd) c in
   let mvty = Typing.meta_type evd mv in
   w_coerce_to_type env evd c cty mvty
 
 let unify_to_type env evd flags c u =
-  let sigma = evars_of evd in
+  let sigma =  evd in
   let c = refresh_universes c in
   let t = get_type_of_with_meta env sigma (metas_of evd) c in
   let t = Tacred.hnf_constr env sigma (nf_betaiota sigma (nf_meta evd t)) in
@@ -518,7 +518,7 @@ let order_metas metas =
 
 let solve_simple_evar_eqn env evd ev rhs =
   let evd,b = solve_simple_eqn Evarconv.evar_conv_x env evd (CONV,ev,rhs) in
-  if not b then error_cannot_unify env (evars_of evd) (mkEvar ev,rhs);
+  if not b then error_cannot_unify env ( evd) (mkEvar ev,rhs);
   let (evd,b) = Evarconv.consider_remaining_unif_problems env evd in
   if not b then error "Cannot solve unification constraints";
   evd
@@ -534,16 +534,16 @@ let w_merge env with_types flags (metas,evars) evd =
     match evars with
     | ((evn,_ as ev),rhs)::evars' ->
     	if is_defined_evar evd ev then
-	  let v = Evd.existential_value (evars_of evd) ev in
+	  let v = Evd.existential_value ( evd) ev in
 	  let (metas',evars'') =
-	    unify_0 env (evars_of evd) topconv flags rhs v in
+	    unify_0 env ( evd) topconv flags rhs v in
 	  w_merge_rec evd (metas'@metas) (evars''@evars') eqns
     	else begin
           let rhs' = subst_meta_instances metas rhs in
           match kind_of_term rhs with
 	  | App (f,cl) when is_mimick_head f & occur_meta rhs' ->
 	      if occur_evar evn rhs' then
-                error_occur_check env (evars_of evd) evn rhs';
+                error_occur_check env ( evd) evn rhs';
 	      let evd' = mimick_evar evd flags f (Array.length cl) evn in
 	      w_merge_rec evd' metas evars eqns
           | _ ->
@@ -568,7 +568,7 @@ let w_merge env with_types flags (metas,evars) evd =
     	if meta_defined evd mv then
 	  let {rebus=c'},(status',_) = meta_fvalue evd mv in
           let (take_left,st,(metas',evars')) =
-	    merge_instances env (evars_of evd) flags status' status c' c
+	    merge_instances env ( evd) flags status' status c' c
 	  in
 	  let evd' = 
             if take_left then evd 
@@ -588,16 +588,16 @@ let w_merge env with_types flags (metas,evars) evd =
     | [] -> evd
 		
   and mimick_evar evd flags hdc nargs sp =
-    let ev = Evd.find (evars_of evd) sp in
+    let ev = Evd.find ( evd) sp in
     let sp_env = Global.env_of_context ev.evar_hyps in
     let (evd', c) = applyHead sp_env evd nargs hdc in
     let (mc,ec) =
-      unify_0 sp_env (evars_of evd') Cumul flags
-        (Retyping.get_type_of_with_meta sp_env (evars_of evd') (metas_of evd') c) ev.evar_concl in
+      unify_0 sp_env ( evd') Cumul flags
+        (Retyping.get_type_of_with_meta sp_env ( evd') (metas_of evd') c) ev.evar_concl in
     let evd'' = w_merge_rec evd' mc ec [] in
-    if (evars_of evd') == (evars_of evd'')
-    then Evd.evar_define sp c evd''
-    else Evd.evar_define sp (Evarutil.nf_evar (evars_of evd'') c) evd'' in
+    if ( evd') == ( evd'')
+    then Evd.define sp c evd''
+    else Evd.define sp (Evarutil.nf_evar ( evd'') c) evd'' in
 
   (* merge constraints *)
   w_merge_rec evd (order_metas metas) evars []
@@ -617,9 +617,9 @@ let w_unify_meta_types env ?(flags=default_unify_flags) evd =
    types of metavars are unifiable with the types of their instances    *)
 
 let check_types env evd flags subst m n =
-  let sigma = evars_of evd in
+  let sigma =  evd in
   if isEvar (fst (whd_stack sigma m)) or isEvar (fst (whd_stack sigma n)) then
-    unify_0_with_initial_metas subst true env (evars_of evd) topconv 
+    unify_0_with_initial_metas subst true env ( evd) topconv 
       flags
       (Retyping.get_type_of_with_meta env sigma (metas_of evd) m)
       (Retyping.get_type_of_with_meta env sigma (metas_of evd) n)
@@ -630,7 +630,7 @@ let w_unify_core_0 env with_types cv_pb flags m n evd =
   let (mc1,evd') = retract_coercible_metas evd in
   let subst1 = check_types env evd flags (mc1,[]) m n in
   let subst2 =
-     unify_0_with_initial_metas subst1 true env (evars_of evd') cv_pb flags m n
+     unify_0_with_initial_metas subst1 true env ( evd') cv_pb flags m n
   in 
   w_merge env with_types flags subst2 evd'
 
@@ -743,8 +743,8 @@ let secondOrderAbstraction env flags allow_K typ (p, oplist) evd =
   w_merge env false flags ([p,pred,(ConvUpToEta 0,TypeProcessed)],[]) evd'
 
 let w_unify2 env flags allow_K cv_pb ty1 ty2 evd =
-  let c1, oplist1 = whd_stack (evars_of evd) ty1 in
-  let c2, oplist2 = whd_stack (evars_of evd) ty2 in
+  let c1, oplist1 = whd_stack ( evd) ty1 in
+  let c2, oplist2 = whd_stack ( evd) ty2 in
   match kind_of_term c1, kind_of_term c2 with
     | Meta p1, _ ->
         (* Find the predicate *)
@@ -782,8 +782,8 @@ let w_unify2 env flags allow_K cv_pb ty1 ty2 evd =
    Meta(1) had meta-variables in it. *)
 let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
   let cv_pb = of_conv_pb cv_pb in
-  let hd1,l1 = whd_stack (evars_of evd) ty1 in
-  let hd2,l2 = whd_stack (evars_of evd) ty2 in
+  let hd1,l1 = whd_stack ( evd) ty1 in
+  let hd2,l2 = whd_stack ( evd) ty2 in
     match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with
       (* Pattern case *)
       | (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true)