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

9 files changed, 112 insertions, 112 deletions

diff --git a/contrib/subtac/equations.ml4 b/contrib/subtac/equations.ml4
index ebbb5505f6..5b76c95871 100644
--- a/contrib/subtac/equations.ml4
+++ b/contrib/subtac/equations.ml4
@@ -880,9 +880,9 @@ let interp_pats i isevar env impls pat sign recu =
 			  str "Error parsing pattern: unnexpected left-hand side")
   in
     isevar := nf_evar_defs !isevar;
-    (nf_rel_context_evar (Evd.evars_of !isevar) varsctx, 
-    nf_env_evar (Evd.evars_of !isevar) env',
-    rev_map (nf_evar (Evd.evars_of !isevar)) pats)
+    (nf_rel_context_evar ( !isevar) varsctx, 
+    nf_env_evar ( !isevar) env',
+    rev_map (nf_evar ( !isevar)) pats)
       
 let interp_eqn i isevar env impls sign arity recu (pats, rhs) =
   let ctx, env', patcs = interp_pats i isevar env impls pats sign recu in
@@ -916,8 +916,8 @@ let define_by_eqs with_comp i (l,ann) t nt eqs =
   let isevar = ref (create_evar_defs Evd.empty) in
   let (env', sign), impls = interp_context_evars isevar env l in
   let arity = interp_type_evars isevar env' t in
-  let sign = nf_rel_context_evar (Evd.evars_of !isevar) sign in
-  let arity = nf_evar (Evd.evars_of !isevar) arity in
+  let sign = nf_rel_context_evar ( !isevar) sign in
+  let arity = nf_evar ( !isevar) arity in
   let arity = 
     if with_comp then
       let compid = add_suffix i "_comp" in
@@ -942,11 +942,11 @@ let define_by_eqs with_comp i (l,ann) t nt eqs =
       Option.iter (Command.declare_interning_data data) nt;
       map (interp_eqn i isevar fixenv data sign arity None) eqs) ()
   in
-  let sign = nf_rel_context_evar (Evd.evars_of !isevar) sign in
-  let arity = nf_evar (Evd.evars_of !isevar) arity in
+  let sign = nf_rel_context_evar ( !isevar) sign in
+  let arity = nf_evar ( !isevar) arity in
   let prob = (i, sign, arity) in
-  let fixenv = nf_env_evar (Evd.evars_of !isevar) fixenv in
-  let fixdecls = nf_rel_context_evar (Evd.evars_of !isevar) fixdecls in
+  let fixenv = nf_env_evar ( !isevar) fixenv in
+  let fixdecls = nf_rel_context_evar ( !isevar) fixdecls in
     (*   let ce = check_evars fixenv Evd.empty !isevar in *)
     (*   List.iter (function (_, _, Program rhs) -> ce rhs | _ -> ()) equations; *)
   let is_recursive, env' =
@@ -966,7 +966,7 @@ let define_by_eqs with_comp i (l,ann) t nt eqs =
     else t, ty
   in
   let obls, t', ty' = 
-    Eterm.eterm_obligations env i !isevar (Evd.evars_of undef) 0 ~status t ty
+    Eterm.eterm_obligations env i !isevar ( undef) 0 ~status t ty
   in
     if is_recursive then
       ignore(Subtac_obligations.add_mutual_definitions [(i, t', ty', impls, obls)] [] 
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 09ee456d7c..00ed62ac88 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -310,7 +310,7 @@ let unify_tomatch_with_patterns isevars env loc typ pats =
     | None -> NotInd (None,typ)
     | Some (_,(ind,_)) ->
 	inh_coerce_to_ind isevars env typ ind;
-	try IsInd (typ,find_rectype env (Evd.evars_of !isevars) typ)
+	try IsInd (typ,find_rectype env ( !isevars) typ)
 	with Not_found -> NotInd (None,typ)
 
 let find_tomatch_tycon isevars env loc = function
@@ -324,9 +324,9 @@ let coerce_row typing_fun isevars env pats (tomatch,(_,indopt)) =
   let j = typing_fun tycon env tomatch in
   let evd, j = Coercion.inh_coerce_to_base (loc_of_rawconstr tomatch) env !isevars j in
   isevars := evd;
-  let typ = nf_evar (Evd.evars_of !isevars) j.uj_type in
+  let typ = nf_evar ( !isevars) j.uj_type in
   let t =
-    try IsInd (typ,find_rectype env (Evd.evars_of !isevars) typ)
+    try IsInd (typ,find_rectype env ( !isevars) typ)
     with Not_found ->
       unify_tomatch_with_patterns isevars env loc typ pats in
   (j.uj_val,t)
@@ -348,7 +348,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps) =
      the first pattern type and forget about the others *)
   let typ = match typ with IsInd (t,_) -> t | NotInd (_,t) -> t in
   let typ =
-    try IsInd (typ,find_rectype pb.env (Evd.evars_of !(pb.isevars)) typ)
+    try IsInd (typ,find_rectype pb.env ( !(pb.isevars)) typ)
     with Not_found -> NotInd (None,typ) in
   let tomatch = ((current,typ),deps) in
   match typ with
@@ -366,7 +366,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps) =
 	      else
 		(evd_comb2 (Coercion.inh_conv_coerce_to dummy_loc pb.env)
 		  pb.isevars (make_judge current typ) (mk_tycon_type indt)).uj_val in
-	    let sigma = Evd.evars_of !(pb.isevars) in
+	    let sigma =  !(pb.isevars) in
 	    let typ = IsInd (indt,find_rectype pb.env sigma indt) in
 	    ((current,typ),deps))
   | _ -> tomatch
@@ -799,7 +799,7 @@ let shift_operator k = function OpLambda _ | OpProd _ -> k+1 | _ -> k
 
 let reloc_operator (k,n) = function OpRel p when p > k -> 
 let rec unify_clauses k pv =
-  let pv'= Array.map (fun (n,sign,_,p) -> n,splay_constr (whd_betaiotaevar (push_rels (List.rev sign) env) (Evd.evars_of isevars)) p) pv in
+  let pv'= Array.map (fun (n,sign,_,p) -> n,splay_constr (whd_betaiotaevar (push_rels (List.rev sign) env) ( isevars)) p) pv in
   let n1,op1 = let (n1,(op1,args1)) = pv'.(0) in n1,op1 in
   if Array.for_all (fun (ni,(opi,_)) -> eq_operator_lift k (n1,ni) (op1,opi)) pv'
   then
@@ -822,7 +822,7 @@ let infer_predicate loc env isevars typs cstrs indf =
     (* Empiric normalization: p may depend in a irrelevant way on args of the*)
     (* cstr as in [c:{_:Alpha & Beta}] match c with (existS a b)=>(a,b) end *)
     let typs =
-      Array.map (local_strong whd_beta (Evd.evars_of !isevars)) typs
+      Array.map (local_strong whd_beta ( !isevars)) typs
     in
     let eqns = array_map2 prepare_unif_pb typs cstrs in
     (* First strategy: no dependencies at all *)
@@ -846,7 +846,7 @@ let infer_predicate loc env isevars typs cstrs indf =
       (true,pred) (* true = dependent -- par défaut *)
     else
 (*
-      let s = get_sort_of env (evars_of isevars) typs.(0) in
+      let s = get_sort_of env ( isevars) typs.(0) in
       let predpred = it_mkLambda_or_LetIn (mkSort s) sign in
       let caseinfo = make_default_case_info mis in
       let brs = array_map2 abstract_conclusion typs cstrs in
@@ -1040,11 +1040,11 @@ let find_predicate loc env isevars p typs cstrs current
   (IndType (indf,realargs)) tms =
   let (dep,pred) =
     match p with
-      | Some p -> abstract_predicate env (Evd.evars_of !isevars) indf current tms p
+      | Some p -> abstract_predicate env ( !isevars) indf current tms p
       | None -> infer_predicate loc env isevars typs cstrs indf in
-  let typ = whd_beta (Evd.evars_of !isevars) (applist (pred, realargs)) in
+  let typ = whd_beta ( !isevars) (applist (pred, realargs)) in
   if dep then
-    (pred, whd_beta (Evd.evars_of !isevars) (applist (typ, [current])),
+    (pred, whd_beta ( !isevars) (applist (typ, [current])),
      new_Type ())
   else
     (pred, typ, new_Type ())
@@ -1271,7 +1271,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 (Evd.evars_of !(pb.isevars)) (deppat,nondeppat,d,t) pb.mat in
+    insert_aliases pb.env ( !(pb.isevars)) (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 *)
@@ -1427,14 +1427,14 @@ let oldprepare_predicate_from_tycon loc dep env isevars tomatchs sign c =
   let n, allargs, env, signs = List.fold_left cook (0, [], env, []) tomatchs in
   let names = List.rev (List.map (List.map pi1) signs) in
   let allargs =
-    List.map (fun c -> lift n (nf_betadeltaiota env (Evd.evars_of !isevars) c)) allargs in
+    List.map (fun c -> lift n (nf_betadeltaiota env ( !isevars) c)) allargs in
   let rec build_skeleton env c =
     (* Don't put into normal form, it has effects on the synthesis of evars *)
- (* let c = whd_betadeltaiota env (evars_of isevars) c in *)
+ (* let c = whd_betadeltaiota env ( isevars) c in *)
     (* We turn all subterms possibly dependent into an evar with maximum ctxt*)
     if isEvar c or List.exists (eq_constr c) allargs then
       e_new_evar isevars env  ~src:(loc, Evd.CasesType)
-        (Retyping.get_type_of env (Evd.evars_of !isevars) c)
+        (Retyping.get_type_of env ( !isevars) c)
     else
       map_constr_with_full_binders push_rel build_skeleton env c 
   in
@@ -1595,7 +1595,7 @@ let constr_of_pat env isevars arsign pat avoid =
 	  PatVar (l, name), [name, None, ty] @ realargs, mkRel 1, ty, (List.map (fun x -> mkRel 1) realargs), 1, avoid
     | PatCstr (l,((_, i) as cstr),args,alias) ->
 	let cind = inductive_of_constructor cstr in
-	let IndType (indf, _) = find_rectype env (Evd.evars_of !isevars) (lift (-(List.length realargs)) ty) in
+	let IndType (indf, _) = find_rectype env ( !isevars) (lift (-(List.length realargs)) ty) in
 	let ind, params = dest_ind_family indf in
 	if ind <> cind then error_bad_constructor_loc l cstr ind;
 	let cstrs = get_constructors env indf in
@@ -1619,8 +1619,8 @@ let constr_of_pat env isevars arsign pat avoid =
 	let cstr = mkConstruct ci.cs_cstr in
 	let app = applistc cstr (List.map (lift (List.length sign)) params) in
 	let app = applistc app args in
-	let apptype = Retyping.get_type_of env (Evd.evars_of !isevars) app in	
-	let IndType (indf, realargs) = find_rectype env (Evd.evars_of !isevars) apptype in
+	let apptype = Retyping.get_type_of env ( !isevars) app in	
+	let IndType (indf, realargs) = find_rectype env ( !isevars) apptype in
 	  match alias with
 	      Anonymous ->
 		pat', sign, app, apptype, realargs, n, avoid
@@ -2047,14 +2047,14 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra
 	  (* Build the dependent arity signature, the equalities which makes
 	     the first part of the predicate and their instantiations. *)
 	let avoid = [] in
-	  build_dependent_signature env (Evd.evars_of !isevars) avoid tomatchs arsign
+	  build_dependent_signature env ( !isevars) avoid tomatchs arsign
 
       in
       let tycon, arity = 
 	match valcon_of_tycon tycon with
 	| None -> let ev = mkExistential env isevars in ev, ev
 	| Some t -> 
-	    t, prepare_predicate_from_arsign_tycon loc env (Evd.evars_of !isevars)
+	    t, prepare_predicate_from_arsign_tycon loc env ( !isevars)
 	      tomatchs sign (lift tomatchs_len t)
       in
       let neqs, arity = 
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 15729b6266..8ef2153464 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -30,7 +30,7 @@ open Util
 module SPretyping = Subtac_pretyping.Pretyping
 
 let interp_binder_evars evdref env na t =
-  let t = Constrintern.intern_gen true (Evd.evars_of !evdref) env t in
+  let t = Constrintern.intern_gen true ( !evdref) env t in
     SPretyping.understand_tcc_evars evdref env IsType t
 
 let interp_binders_evars isevars env avoid l =
@@ -65,7 +65,7 @@ let interp_constrs_evars isevars env avoid l =
     
 let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c =
   SPretyping.understand_tcc_evars evdref env kind
-    (intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c)
+    (intern_gen (kind=IsType) ~impls ( !evdref) env c)
 
 let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ =
   interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c
@@ -94,7 +94,7 @@ let substitution_of_constrs ctx cstrs =
 
 let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) pri =
   let env = Global.env() in
-  let isevars = ref (Evd.create_evar_defs Evd.empty) in
+  let isevars = ref Evd.empty in
   let tclass =
     match bk with
     | Implicit ->
@@ -134,7 +134,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
   let env' = push_rel_context ctx' env in
   isevars := Evarutil.nf_evar_defs !isevars;
   isevars := resolve_typeclasses ~onlyargs:false ~fail:true env' !isevars;
-  let sigma = Evd.evars_of !isevars in
+  let sigma =  !isevars in
   let subst = List.map (Evarutil.nf_evar sigma) subst in
   let subst = 
     let props = 
@@ -188,7 +188,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
 	Impargs.declare_manual_implicits false gr ~enriching:false imps;
 	Typeclasses.add_instance inst
     in
-    let evm = Subtac_utils.evars_of_term (Evd.evars_of !isevars) Evd.empty term in
+    let evm = Subtac_utils.evars_of_term ( !isevars) Evd.empty term in
     let obls, constr, typ = Eterm.eterm_obligations env id !isevars evm 0 term termtype in
       id, Subtac_obligations.add_definition id constr typ ~kind:(Global,false,Instance) ~hook obls
 	
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 0af732f858..54114b0b06 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -83,7 +83,7 @@ module Coercion = struct
       | Type _, Prop Null -> Prop Null
       | _, Type _ -> s2
 
-  let hnf env isevars c = whd_betadeltaiota env (evars_of !isevars) c
+  let hnf env isevars c = whd_betadeltaiota env ( !isevars) c
 
   let lift_args n sign =
     let rec liftrec k = function
@@ -109,7 +109,7 @@ module Coercion = struct
   and coerce loc env isevars (x : Term.constr) (y : Term.constr) 
       : (Term.constr -> Term.constr) option 
       =
-    let x = nf_evar (evars_of !isevars) x and y = nf_evar (evars_of !isevars) y in
+    let x = nf_evar ( !isevars) x and y = nf_evar ( !isevars) y in
     let rec coerce_unify env x y =
       let x = hnf env isevars x and y = hnf env isevars y in
 	try 
@@ -119,7 +119,7 @@ module Coercion = struct
     and coerce' env x y : (Term.constr -> Term.constr) option =
       let subco () = subset_coerce env isevars x y in
       let dest_prod c =
-	match Reductionops.splay_prod_n env (evars_of !isevars) 1 c with
+	match Reductionops.splay_prod_n env ( !isevars) 1 c with
 	| [(na,b,t)], c -> (na,t), c
 	| _ -> raise NoSubtacCoercion
       in
@@ -209,7 +209,7 @@ module Coercion = struct
 				       isevars := evs;
 				       let (n, dom, rng) = destLambda t in
 				       let (domk, args) = destEvar dom in
-					 isevars := evar_define domk a !isevars;
+					 isevars := define domk a !isevars;
 					 t, rng
 				 | _ -> raise NoSubtacCoercion
 			     in
@@ -252,7 +252,7 @@ module Coercion = struct
 			   end
 		       else
 			 if i = i' && len = Array.length l' then
-			   let evm = evars_of !isevars in
+			   let evm =  !isevars in
 			     (try subco () 
 			       with NoSubtacCoercion ->
 				 let typ = Typing.type_of env evm c in
@@ -264,7 +264,7 @@ module Coercion = struct
 			   subco ()
 		 | x, y when x = y ->
 		     if Array.length l = Array.length l' then
-		       let evm = evars_of !isevars in
+		       let evm =  !isevars in
 		       let lam_type = Typing.type_of env evm c in
 		       let lam_type' = Typing.type_of env evm c' in
 (* 			 if not (is_arity env evm lam_type) then ( *)
@@ -357,7 +357,7 @@ module Coercion = struct
     with _ -> anomaly "apply_coercion"
 
   let inh_app_fun env isevars j = 
-    let t = whd_betadeltaiota env (evars_of isevars) j.uj_type in
+    let t = whd_betadeltaiota env ( isevars) j.uj_type in
       match kind_of_term t with
 	| Prod (_,_,_) -> (isevars,j)
 	| Evar ev when not (is_defined_evar isevars ev) ->
@@ -366,8 +366,8 @@ module Coercion = struct
 	| _ ->
        	    (try
       	       let t,p =
-		 lookup_path_to_fun_from env (evars_of isevars) j.uj_type in
-		 (isevars,apply_coercion env (evars_of isevars) p j t)
+		 lookup_path_to_fun_from env ( isevars) j.uj_type in
+		 (isevars,apply_coercion env ( isevars) p j t)
 	     with Not_found ->
 	       try 
 		 let coercef, t = mu env isevars t in
@@ -377,14 +377,14 @@ module Coercion = struct
 
   let inh_tosort_force loc env isevars j =
     try
-      let t,p = lookup_path_to_sort_from env (evars_of isevars) j.uj_type in
-      let j1 = apply_coercion env (evars_of isevars) p j t in 
-	(isevars,type_judgment env (j_nf_evar (evars_of isevars) j1))
+      let t,p = lookup_path_to_sort_from env ( isevars) j.uj_type in
+      let j1 = apply_coercion env ( isevars) p j t in 
+	(isevars,type_judgment env (j_nf_evar ( isevars) j1))
     with Not_found ->
-      error_not_a_type_loc loc env (evars_of isevars) j
+      error_not_a_type_loc loc env ( isevars) j
 
   let inh_coerce_to_sort loc env isevars j =
-    let typ = whd_betadeltaiota env (evars_of isevars) j.uj_type in
+    let typ = whd_betadeltaiota env ( isevars) j.uj_type in
       match kind_of_term typ with
 	| Sort s -> (isevars,{ utj_val = j.uj_val; utj_type = s })
 	| Evar ev when not (is_defined_evar isevars ev) ->
@@ -394,13 +394,13 @@ module Coercion = struct
 	    inh_tosort_force loc env isevars j
 
   let inh_coerce_to_base loc env isevars j =
-    let typ = whd_betadeltaiota env (evars_of isevars) j.uj_type in
+    let typ = whd_betadeltaiota env ( isevars) j.uj_type in
     let ct, typ' = mu env isevars typ in
       isevars, { uj_val = app_opt ct j.uj_val; 
 		 uj_type = typ' }
 
   let inh_coerce_to_prod loc env isevars t =
-    let typ = whd_betadeltaiota env (evars_of isevars) (snd t) in
+    let typ = whd_betadeltaiota env ( isevars) (snd t) in
     let _, typ' = mu env isevars typ in
       isevars, (fst t, typ')
 	
@@ -411,10 +411,10 @@ module Coercion = 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
+		let j = apply_coercion env ( evd) p
 		  {uj_val = v; uj_type = t} t2 in
 		  Some j.uj_val, j.uj_type
 	    | None -> None, t
@@ -430,8 +430,8 @@ module Coercion = 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. *)
@@ -463,7 +463,7 @@ module Coercion = struct
 		(Some (nf_isevar evd cj.uj_val))
 		(nf_isevar evd cj.uj_type) (nf_isevar evd t)
 	    with NoCoercion ->
-	      let sigma = evars_of evd in
+	      let sigma =  evd in
 		try
 		  coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t
 		with NoSubtacCoercion ->
@@ -484,7 +484,7 @@ module Coercion = struct
 	| Some (init, cur) -> init, cur
     in
       try 
-	let rels, rng = Reductionops.splay_prod_n env (evars_of isevars) nabs t in
+	let rels, rng = Reductionops.splay_prod_n env ( isevars) nabs t in
 	(* The final range free variables must have been replaced by evars, we accept only that evars
 	   in rng are applied to free vars. *)
 	if noccur_with_meta 1 (succ nabs) rng then (
@@ -497,7 +497,7 @@ module Coercion = struct
 		   with NoCoercion ->
 		     coerce_itf loc env' isevars None t t')
 	    with NoSubtacCoercion ->
-	      let sigma = evars_of isevars in
+	      let sigma =  isevars in
 		error_cannot_coerce env' sigma (t, t'))
 	else isevars
       with _ -> isevars
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 4876b06555..674805962d 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -57,7 +57,7 @@ let evar_nf isevars c =
 let interp_gen kind isevars env 
                ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
                c =
-  let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars (Evd.evars_of !isevars) env c in
+  let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars ( !isevars) env c in
   let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in
     evar_nf isevars c'
 
@@ -75,14 +75,14 @@ let interp_casted_constr_evars isevars env ?(impls=([],[])) c typ =
 
 let interp_open_constr isevars env c =
     msgnl (str "Pretyping " ++ my_print_constr_expr c);
-  let c = Constrintern.intern_constr (Evd.evars_of !isevars) env c in
+  let c = Constrintern.intern_constr ( !isevars) env c in
   let c' = SPretyping.pretype_gen isevars env ([], []) (OfType None) c in
     evar_nf isevars c'
 
 let interp_constr_judgment isevars env c =
   let j = 
     SPretyping.understand_judgment_tcc isevars env
-      (Constrintern.intern_constr (Evd.evars_of !isevars) env c) 
+      (Constrintern.intern_constr ( !isevars) env c) 
   in
     { uj_val = evar_nf isevars j.uj_val; uj_type = evar_nf isevars j.uj_type }
 
@@ -95,11 +95,11 @@ let locate_if_isevar loc na = function
   | x -> x
 
 let interp_binder sigma env na t =
-  let t = Constrintern.intern_gen true (Evd.evars_of !sigma) env t in
+  let t = Constrintern.intern_gen true ( !sigma) env t in
     SPretyping.pretype_gen sigma env ([], []) IsType (locate_if_isevar (loc_of_rawconstr t) na t)
 
 let interp_context_evars evdref env params = 
-  let bl = Constrintern.intern_context false (Evd.evars_of !evdref) env params in
+  let bl = Constrintern.intern_context false ( !evdref) env params in
   let (env, par, _, impls) =
     List.fold_left
       (fun (env,params,n,impls) (na, k, b, t) ->
@@ -299,8 +299,8 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   let typ = it_mkProd_or_LetIn top_arity binders_rel in
   let fullcoqc = Evarutil.nf_isevar !isevars def in
   let fullctyp = Evarutil.nf_isevar !isevars typ in
-  let evm = evars_of_term (Evd.evars_of !isevars) Evd.empty fullctyp in
-  let evm = evars_of_term (Evd.evars_of !isevars) evm fullcoqc in
+  let evm =evars_of_term ( !isevars) Evd.empty fullctyp in
+  let evm = evars_of_term ( !isevars) evm fullcoqc in
   let evm = non_instanciated_map env isevars evm in
   let evars, evars_def, evars_typ = Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp in
     Subtac_obligations.add_definition recname evars_def evars_typ ~implicits:impls evars
@@ -351,7 +351,7 @@ let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype =
 let push_named_context = List.fold_right push_named
 
 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
@@ -374,7 +374,7 @@ let interp_recursive fixkind l boxed =
   let fixnames = List.map (fun fix -> fix.Command.fix_name) fixl in
 
   (* Interp arities allowing for unresolved types *)
-  let evdref = ref (Evd.create_evar_defs Evd.empty) in
+  let evdref = ref Evd.empty in
   let fixctxs, fiximps = List.split (List.map (interp_fix_context evdref env) fixl) in
   let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in
   let fixtypes = List.map2 build_fix_type fixctxs fixccls in
@@ -397,9 +397,9 @@ let interp_recursive fixkind l boxed =
 
   (* Instantiate evars and check all are resolved *)
   let evd,_ = Evarconv.consider_remaining_unif_problems env_rec !evdref in
-  let fixdefs = List.map (nf_evar (evars_of evd)) fixdefs in
-  let fixtypes = List.map (nf_evar (evars_of evd)) fixtypes in
-  let rec_sign = nf_named_context_evar (evars_of evd) rec_sign in
+  let fixdefs = List.map (nf_evar ( evd)) fixdefs in
+  let fixtypes = List.map (nf_evar ( evd)) fixtypes in
+  let rec_sign = nf_named_context_evar ( evd) rec_sign in
     
   let recdefs = List.length rec_sign in
   List.iter (check_evars env_rec Evd.empty evd) fixdefs;
@@ -410,7 +410,7 @@ let interp_recursive fixkind l boxed =
 
   (* Get the interesting evars, those that were not instanciated *)
   let isevars = Evd.undefined_evars evd in
-  let evm = Evd.evars_of isevars in
+  let evm =  isevars in
   (* Solve remaining evars *)
   let rec collect_evars id def typ imps = 
       (* Generalize by the recursive prototypes  *)
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index 0159de5427..d9df5b34c1 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -74,7 +74,7 @@ let interp env isevars c tycon =
   let evd,_ = consider_remaining_unif_problems env !isevars in
 (*   let unevd = undefined_evars evd in *)
   let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true ~fail:true env evd in
-  let evm = evars_of unevd' in
+  let evm =  unevd' in
     isevars := unevd';
     nf_evar evm j.uj_val, nf_evar evm j.uj_type
 
@@ -86,8 +86,8 @@ let find_with_index x l =
 
 open Vernacexpr
 
-let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr (evars_of evd) env
-let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_type (evars_of evd) env
+let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr ( evd) env
+let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_type ( evd) env
 
 let env_with_binders env isevars l =
   let rec aux ((env, rels) as acc) = function
@@ -123,7 +123,7 @@ let subtac_process env isevars id bl c tycon =
   let c = coqintern_constr !isevars env c in
   let imps = Implicit_quantifiers.implicits_of_rawterm c in
   let coqc, ctyp = interp env isevars c tycon in
-  let evm = non_instanciated_map env isevars (evars_of !isevars) in
+  let evm = non_instanciated_map env isevars ( !isevars) in
   let ty = nf_isevar !isevars (match tycon with Some (None, c) -> c | _ -> ctyp) in
     evm, coqc, ty, imps
 
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 023213ecbc..01fe4ef6f1 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -79,14 +79,14 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	for i = 0 to lt-1 do 
           if not (e_cumul env isevars (vdefj.(i)).uj_type
 		    (lift lt lar.(i))) then
-            error_ill_typed_rec_body_loc loc env (evars_of !isevars)
+            error_ill_typed_rec_body_loc loc env ( !isevars)
               i lna vdefj lar
 	done
 
   let check_branches_message loc env isevars c (explft,lft) = 
     for i = 0 to Array.length explft - 1 do
       if not (e_cumul env isevars lft.(i) explft.(i)) then 
-	let sigma = evars_of !isevars in
+	let sigma =  !isevars in
 	  error_ill_formed_branch_loc loc env sigma c i lft.(i) explft.(i)
     done
 
@@ -99,7 +99,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 
   (*
     let evar_type_case isevars env ct pt lft p c =
-    let (mind,bty,rslty) = type_case_branches env (evars_of isevars) ct pt p c
+    let (mind,bty,rslty) = type_case_branches env ( isevars) ct pt p c
     in check_branches_message isevars env (c,ct) (bty,lft); (mind,rslty)
   *)
 
@@ -158,7 +158,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
     | RType _ -> judge_of_new_Type ()
 
   (* [pretype tycon env isevars lvar lmeta cstr] attempts to type [cstr] *)
-  (* in environment [env], with existential variables [(evars_of isevars)] and *)
+  (* in environment [env], with existential variables [( isevars)] and *)
   (* the type constraint tycon *)
   let rec pretype (tycon : type_constraint) env isevars lvar c = 
 (*     let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_rawconstr env c ++ *)
@@ -179,12 +179,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
     | REvar (loc, ev, 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_context (Evd.find (evars_of !isevars) ev) in
+	let hyps = evar_context (Evd.find ( !isevars) ev) in
 	let args = match instopt with
           | None -> instance_from_named_context hyps
           | Some inst -> failwith "Evar subtitutions not implemented" in
 	let c = mkEvar (ev, args) in
-	let j = (Retyping.get_judgment_of env (evars_of !isevars) c) in
+	let j = (Retyping.get_judgment_of env ( !isevars) c) in
 	  inh_conv_coerce_to_tycon loc env isevars j tycon
 
     | RPatVar (loc,(someta,n)) -> 
@@ -246,8 +246,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		  uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
             ctxtv vdef in
 	evar_type_fixpoint loc env isevars names ftys vdefj;
-	let ftys = Array.map (nf_evar (evars_of !isevars)) ftys in
-	let fdefs = Array.map (fun x -> nf_evar (evars_of !isevars) (j_val x)) vdefj in
+	let ftys = Array.map (nf_evar ( !isevars)) ftys in
+	let fdefs = Array.map (fun x -> nf_evar ( !isevars) (j_val x)) vdefj in
 	let fixj = match fixkind with
 	  | RFix (vn,i) ->
 	      (* First, let's find the guard indexes. *)
@@ -297,7 +297,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  | c::rest ->
 	      let argloc = loc_of_rawconstr c in
 	      let resj = evd_comb1 (Coercion.inh_app_fun env) isevars resj in
-              let resty = whd_betadeltaiota env (evars_of !isevars) resj.uj_type in
+              let resty = whd_betadeltaiota env ( !isevars) resj.uj_type in
       		match kind_of_term resty with
 		  | Prod (na,c1,c2) ->
 		      Option.iter (fun ty -> isevars :=
@@ -315,14 +315,14 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		  | _ ->
 		      let hj = pretype empty_tycon env isevars lvar c in
 			error_cant_apply_not_functional_loc 
-			  (join_loc floc argloc) env (evars_of !isevars)
+			  (join_loc floc argloc) env ( !isevars)
 	      		  resj [hj]
 	in
-	let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj ftycon args) in
+	let resj = j_nf_evar ( !isevars) (apply_rec env 1 fj ftycon args) in
 	let resj =
 	  match kind_of_term resj.uj_val with
 	  | App (f,args) when isInd f or isConst f ->
-	      let sigma = evars_of !isevars in
+	      let sigma =  !isevars 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
@@ -369,10 +369,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
     | RLetTuple (loc,nal,(na,po),c,d) ->
 	let cj = pretype empty_tycon env isevars lvar c in
 	let (IndType (indf,realargs)) = 
-	  try find_rectype env (evars_of !isevars) cj.uj_type
+	  try find_rectype env ( !isevars) cj.uj_type
 	  with Not_found ->
 	    let cloc = loc_of_rawconstr c in
-	      error_case_not_inductive_loc cloc env (evars_of !isevars) cj 
+	      error_case_not_inductive_loc cloc env ( !isevars) cj 
 	in
 	let cstrs = get_constructors env indf in
 	if Array.length cstrs <> 1 then
@@ -396,14 +396,14 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		 | Some p ->
 		     let env_p = push_rels psign env in
 		     let pj = pretype_type empty_valcon env_p isevars lvar p in
-		     let ccl = nf_evar (evars_of !isevars) pj.utj_val in
+		     let ccl = nf_evar ( !isevars) pj.utj_val in
 		     let psign = make_arity_signature env true indf in (* with names *)
 		     let p = it_mkLambda_or_LetIn ccl psign in
 		     let inst = 
 		       (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 !isevars) lp inst in
+		     let fty = hnf_lam_applist env ( !isevars) lp inst in
 		     let fj = pretype (mk_tycon fty) env_f isevars lvar d in
 		     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
 		     let v =
@@ -416,12 +416,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		     let tycon = lift_tycon cs.cs_nargs tycon in
 		     let fj = pretype tycon env_f isevars lvar d in
 		     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
-		     let ccl = nf_evar (evars_of !isevars) fj.uj_type in
+		     let ccl = nf_evar ( !isevars) fj.uj_type in
 		     let ccl =
 		       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 !isevars) 
+			 error_cant_find_case_type_loc loc env ( !isevars) 
 			   cj.uj_val in
 		     let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
 		     let v =
@@ -434,10 +434,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
     | RIf (loc,c,(na,po),b1,b2) ->
 	let cj = pretype empty_tycon env isevars lvar c in
 	let (IndType (indf,realargs)) = 
-	  try find_rectype env (evars_of !isevars) cj.uj_type
+	  try find_rectype env ( !isevars) cj.uj_type
 	  with Not_found ->
 	    let cloc = loc_of_rawconstr c in
-	      error_case_not_inductive_loc cloc env (evars_of !isevars) cj in
+	      error_case_not_inductive_loc cloc env ( !isevars) cj in
 	let cstrs = get_constructors env indf in 
 	  if Array.length cstrs <> 2 then
             user_err_loc (loc,"",
@@ -456,7 +456,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	    | Some p ->
 		let env_p = push_rels psign env in
 		let pj = pretype_type empty_valcon env_p isevars lvar p in
-		let ccl = nf_evar (evars_of !isevars) pj.utj_val in
+		let ccl = nf_evar ( !isevars) 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 isevars {uj_val = pred;
@@ -470,8 +470,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
                       e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ())
 		in
 		  it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
-	  let pred = nf_evar (evars_of !isevars) pred in
-	  let p = nf_evar (evars_of !isevars) p in
+	  let pred = nf_evar ( !isevars) pred in
+	  let p = nf_evar ( !isevars) p in
 	 (*   msgnl (str "Pred is: " ++ Termops.print_constr_env env pred);*)
 	  let f cs b =
 	    let n = rel_context_length cs.cs_args in
@@ -525,7 +525,7 @@ module SubtacPretyping_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 !isevars) c) in
+	  let j = (Retyping.get_judgment_of env ( !isevars) c) in
 	    j
 	      (*inh_conv_coerce_to_tycon loc env isevars j tycon*)
 	else
@@ -537,7 +537,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	(match valcon with
 	   | Some v ->
                let s =
-		 let sigma = evars_of !isevars in
+		 let sigma =  !isevars in
 		 let t = Retyping.get_type_of env sigma v in
 		   match kind_of_term (whd_betadeltaiota env sigma t) with
                      | Sort s -> s
@@ -561,7 +561,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		if e_cumul env isevars v tj.utj_val then tj
 		else
 		  error_unexpected_type_loc
-                    (loc_of_rawconstr c) env (evars_of !isevars) tj.utj_val v
+                    (loc_of_rawconstr c) env ( !isevars) tj.utj_val v
 
   let pretype_gen_aux isevars env lvar kind c =
     let c' = match kind with
@@ -572,12 +572,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  (pretype_type empty_valcon env isevars lvar c).utj_val in
     let evd,_ = consider_remaining_unif_problems env !isevars in
       isevars:=evd;
-      nf_evar (evars_of !isevars) c'
+      nf_evar ( !isevars) c'
 
   let pretype_gen isevars env lvar kind c =
     let c = pretype_gen_aux isevars env lvar kind c in
       isevars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env !isevars;
-      nf_evar (evars_of !isevars) c
+      nf_evar ( !isevars) c
 
   (* TODO: comment faire remonter l'information si le typage a resolu des
      variables du sigma original. il faudrait que la fonction de typage
@@ -587,14 +587,14 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
   let understand_judgment sigma env c =
     let isevars = ref (create_evar_defs sigma) in
     let j = pretype empty_tycon env isevars ([],[]) c in
-    let j = j_nf_evar (evars_of !isevars) j in
+    let j = j_nf_evar ( !isevars) j in
     let isevars,_ = consider_remaining_unif_problems env !isevars in
       check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
       j
 
   let understand_judgment_tcc isevars env c =
     let j = pretype empty_tycon env isevars ([],[]) c in
-    let sigma = evars_of !isevars in
+    let sigma =  !isevars in
     let j = j_nf_evar sigma j in
       j
 
@@ -635,7 +635,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	let c = pretype_gen_aux isevars env ([],[]) (OfType exptyp) c in
 	  !isevars, c
     in
-      Evd.evars_of ev, t
+       ev, t
 end
 
 module Default : S = SubtacPretyping_F(Coercion.Default)
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index cdbc402321..ba30ee1900 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -437,7 +437,7 @@ let pr_evar_info evi =
   in
   hov 2 (str"["  ++ phyps ++ spc () ++ str"|- "  ++ pty ++ pb ++ str"]")
 
-let pr_evar_map sigma =
+let pr_evar_defs sigma =
   h 0 
     (prlist_with_sep pr_fnl
       (fun (ev,evi) ->
@@ -455,9 +455,9 @@ let pr_constraints pbs =
 
 let pr_evar_defs evd =
   let pp_evm =
-    let evars = evars_of evd in
+    let evars =  evd in
     if evars = empty then mt() else
-      str"EVARS:"++brk(0,1)++pr_evar_map evars++fnl() in
+      str"EVARS:"++brk(0,1)++pr_evar_defs evars++fnl() in
   let pp_met =
     if meta_list evd = [] then mt() else
       str"METAS:"++brk(0,1)++pr_meta_map evd in
diff --git a/contrib/xml/proof2aproof.ml b/contrib/xml/proof2aproof.ml
index 30dc7b710e..f7524671fd 100644
--- a/contrib/xml/proof2aproof.ml
+++ b/contrib/xml/proof2aproof.ml
@@ -149,7 +149,7 @@ let extract_open_proof sigma pf =
    in
     let unsharedconstr =
      let evar_nf_constr =
-      nf_evar (Evd.evars_of !evd)
+      nf_evar ( !evd)
         ~preserve:(function e -> S.mem e !unshared_constrs) constr
      in
       Unshare.unshare
@@ -159,14 +159,14 @@ let extract_open_proof sigma pf =
 (*CSC: debugging stuff to be removed *)
 if ProofTreeHash.mem proof_tree_to_constr node then
  Pp.ppnl (Pp.(++) (Pp.str "#DUPLICATE INSERTION: ")
- (Tactic_printer.print_proof (Evd.evars_of !evd) [] node)) ;
+ (Tactic_printer.print_proof ( !evd) [] node)) ;
      ProofTreeHash.add proof_tree_to_constr node unsharedconstr ;
      unshared_constrs := S.add unsharedconstr !unshared_constrs ;
      unsharedconstr
   in
   let unshared_pf = unshare_proof_tree pf in
   let pfterm = proof_extractor [] unshared_pf in
-   (pfterm, Evd.evars_of !evd, proof_tree_to_constr, proof_tree_to_flattened_proof_tree,
+   (pfterm,  !evd, proof_tree_to_constr, proof_tree_to_flattened_proof_tree,
     unshared_pf)
 ;;