Uniformisation politique de nommage evd/isevars (evd si evar_defs,

evdref si evar_defs ref)


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

6 files changed, 514 insertions, 512 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index e76a9745a..6ac1c8a16 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -245,7 +245,7 @@ let push_history_pattern n current cont =
 
 (* A pattern-matching problem has the following form:
 
-   env, isevars |- <pred> Cases tomatch of mat end
+   env, evd |- <pred> Cases tomatch of mat end
 
   where tomatch is some sequence of "instructions" (t1  ... tn)
 
@@ -277,7 +277,7 @@ let push_history_pattern n current cont =
 *)
 type pattern_matching_problem =
     { env      : env;
-      isevars  : Evd.evar_defs ref;
+      evdref   : Evd.evar_defs ref;
       pred     : predicate_signature option;
       tomatch  : tomatch_stack;
       history  : pattern_continuation;
@@ -306,7 +306,7 @@ let rec find_row_ind = function
   | PatVar _ :: l -> find_row_ind l
   | PatCstr(loc,c,_,_) :: _ -> Some (loc,c)
 
-let inductive_template isevars env tmloc ind =
+let inductive_template evdref env tmloc ind =
   let arsign = get_full_arity_sign env ind in
   let hole_source = match tmloc with 
     | Some loc -> fun i -> (loc, Evd.TomatchTypeParameter (ind,i))
@@ -317,59 +317,59 @@ let inductive_template isevars env tmloc ind =
 	match b with
         | None ->
 	    let ty' = substl subst ty in
-	    let e = e_new_evar isevars env ~src:(hole_source n) ty' in
+	    let e = e_new_evar evdref env ~src:(hole_source n) ty' in
 	    (e::subst,e::evarl,n+1) 
 	| Some b ->
 	    (b::subst,evarl,n+1))
       arsign ([],[],1) in
    applist (mkInd ind,List.rev evarl)
 
-let inh_coerce_to_ind isevars env ty tyi =
-  let expected_typ = inductive_template isevars env None tyi in
+let inh_coerce_to_ind evdref env ty tyi =
+  let expected_typ = inductive_template evdref env None tyi in
      (* devrait être indifférent d'exiger leq ou pas puisque pour 
         un inductif cela doit être égal *)
-  let _ = e_cumul env isevars expected_typ ty in ()
+  let _ = e_cumul env evdref expected_typ ty in ()
 
-let unify_tomatch_with_patterns isevars env loc typ pats =
+let unify_tomatch_with_patterns evdref env loc typ pats =
   match find_row_ind pats with
     | 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)
+	inh_coerce_to_ind evdref env typ ind;
+	try IsInd (typ,find_rectype env (Evd.evars_of !evdref) typ)
 	with Not_found -> NotInd (None,typ)
 
-let find_tomatch_tycon isevars env loc = function
+let find_tomatch_tycon evdref env loc = function
   (* Try if some 'in I ...' is present and can be used as a constraint *)
-  | Some (_,ind,_,_) -> mk_tycon (inductive_template isevars env loc ind)
+  | Some (_,ind,_,_) -> mk_tycon (inductive_template evdref env loc ind)
   | None -> empty_tycon
 
-let coerce_row typing_fun isevars env pats (tomatch,(_,indopt)) =
+let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) =
   let loc = Some (loc_of_rawconstr tomatch) in
-  let tycon = find_tomatch_tycon isevars env loc indopt in
+  let tycon = find_tomatch_tycon evdref env loc indopt in
   let j = typing_fun tycon env tomatch in
-  let typ = nf_evar (Evd.evars_of !isevars) j.uj_type in
+  let typ = nf_evar (Evd.evars_of !evdref) j.uj_type in
   let t =
-    try IsInd (typ,find_rectype env (Evd.evars_of !isevars) typ)
+    try IsInd (typ,find_rectype env (Evd.evars_of !evdref) typ)
     with Not_found ->
-      unify_tomatch_with_patterns isevars env loc typ pats in
+      unify_tomatch_with_patterns evdref env loc typ pats in
   (j.uj_val,t)
 
-let coerce_to_indtype typing_fun isevars env matx tomatchl =
+let coerce_to_indtype typing_fun evdref env matx tomatchl =
   let pats = List.map (fun r ->  r.patterns) matx in
   let matx' = match matrix_transpose pats with
     | [] -> List.map (fun _ -> []) tomatchl (* no patterns at all *)
     | m -> m in
-  List.map2 (coerce_row typing_fun isevars env) matx' tomatchl
+  List.map2 (coerce_row typing_fun evdref env) matx' tomatchl
 
 (************************************************************************)
 (* Utils *)
 
-let mkExistential env ?(src=(dummy_loc,Evd.InternalHole)) isevars =
-  e_new_evar isevars env ~src:src (new_Type ())
+let mkExistential env ?(src=(dummy_loc,Evd.InternalHole)) evdref =
+  e_new_evar evdref env ~src:src (new_Type ())
 
-let evd_comb2 f isevars x y =
-  let (evd',y) = f !isevars x y in
-  isevars := evd';
+let evd_comb2 f evdref x y =
+  let (evd',y) = f !evdref x y in
+  evdref := evd';
   y
 
 
@@ -383,7 +383,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 (Evd.evars_of !(pb.evdref)) typ)
     with Not_found -> NotInd (None,typ) in
   let tomatch = ((current,typ),deps) in
   match typ with
@@ -392,25 +392,25 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps) =
       (match find_row_ind tm1 with
 	| None -> tomatch
 	| Some (_,(ind,_)) ->
-	    let indt = inductive_template pb.isevars pb.env None ind in
+	    let indt = inductive_template pb.evdref pb.env None ind in
 	    let current =
 	      if deps = [] & isEvar typ then
 	      (* Don't insert coercions if dependent; only solve evars *)
-		let _ = e_cumul pb.env pb.isevars indt typ in
+		let _ = e_cumul pb.env pb.evdref indt typ in
 		current
 	      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
+		  pb.evdref (make_judge current typ) (mk_tycon_type indt)).uj_val in
+	    let sigma = Evd.evars_of !(pb.evdref) in
 	    let typ = IsInd (indt,find_rectype pb.env sigma indt) in
 	    ((current,typ),deps))
   | _ -> tomatch
 
    (* extract some ind from [t], possibly coercing from constructors in [tm] *)
-let to_mutind env isevars tm c t =
+let to_mutind env evdref tm c t =
 (*  match c with
     | Some body -> *) NotInd (c,t)
-(*    | None -> unify_tomatch_with_patterns isevars env t tm*)
+(*    | None -> unify_tomatch_with_patterns evdref env t tm*)
 
 let type_of_tomatch = function
   | IsInd (t,_) -> t
@@ -831,7 +831,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) (Evd.evars_of evdref)) 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
@@ -846,15 +846,15 @@ let abstract_conclusion typ cs =
   let (sign,p) = decompose_prod_n n typ in
   lam_it p sign
 
-let infer_predicate loc env isevars typs cstrs indf =
-  (* Il faudra substituer les isevars a un certain moment *)
+let infer_predicate loc env evdref typs cstrs indf =
+  (* Il faudra substituer les evdref a un certain moment *)
   if Array.length cstrs = 0 then (* "TODO4-3" *)
     error "Inference of annotation for empty inductive types not implemented"
   else
     (* 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_betaevar empty_env (Evd.evars_of !isevars))) typs
+      Array.map (local_strong (whd_betaevar empty_env (Evd.evars_of !evdref))) typs
     in
     let eqns = array_map2 prepare_unif_pb typs cstrs in
     (* First strategy: no dependencies at all *)
@@ -868,9 +868,9 @@ let infer_predicate loc env isevars typs cstrs indf =
 	(* Heuristic to avoid comparison between non-variables algebric univs*)
 	new_Type ()
       else
-	mkExistential env ~src:(loc, Evd.CasesType) isevars
+	mkExistential env ~src:(loc, Evd.CasesType) evdref
     in
-    if array_for_all (fun (_,_,typ) -> e_cumul env isevars typ mtyp) eqns
+    if array_for_all (fun (_,_,typ) -> e_cumul env evdref typ mtyp) eqns
     then
       (* Non dependent case -> turn it into a (dummy) dependent one *)
       let sign = (Anonymous,None,build_dependent_inductive env indf)::sign in
@@ -878,7 +878,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 (evars_of evdref) 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
@@ -1068,12 +1068,12 @@ let specialize_predicate tomatchs deps cs = function
       (* We finally get gamma,x1..xn |- [X1,x1:=R1,x1]..[Xn,xn:=Rn,xn]pred'''*)
       snd (List.fold_right2 (expand_arg n isdep) tomatchs deps (n,pred'''))
 
-let find_predicate loc env isevars p typs cstrs current
+let find_predicate loc env evdref 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
-      | None -> infer_predicate loc env isevars typs cstrs indf in
+      | Some p -> abstract_predicate env (Evd.evars_of !evdref) indf current tms p
+      | None -> infer_predicate loc env evdref typs cstrs indf in
   let typ = whd_beta (applist (pred, realargs)) in
   if dep then
     (pred, whd_beta (applist (typ, [current])), new_Type ())
@@ -1188,7 +1188,7 @@ let build_branch current deps pb eqns const_info =
       (fun (na,c,t as d) (env,typs,tms) ->
 	 let tm1 = List.map List.hd tms in
 	 let tms = List.map List.tl tms in
- 	 (push_rel d env, (na,to_mutind env pb.isevars tm1 c t)::typs,tms))
+ 	 (push_rel d env, (na,to_mutind env pb.evdref tm1 c t)::typs,tms))
       typs (pb.env,[],List.map fst eqns) in
 
   let dep_sign =
@@ -1274,7 +1274,7 @@ and match_current pb tomatch =
 	  let brvals = Array.map (fun (v,_) -> v) brs in
 	  let brtyps = Array.map (fun (_,t) -> t) brs in
 	  let (pred,typ,s) =
-	    find_predicate pb.caseloc pb.env pb.isevars 
+	    find_predicate pb.caseloc pb.env pb.evdref 
 	      pb.pred brtyps cstrs current indt pb.tomatch in
 	  let ci = make_case_info pb.env mind RegularStyle in
 	  let case = mkCase (ci,nf_betaiota pred,current,brvals) in
@@ -1301,7 +1301,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 (Evd.evars_of !(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 *)
@@ -1350,7 +1350,7 @@ let matx_of_eqns env tomatchl eqns =
 (************************************************************************)
 (* preparing the elimination predicate if any                          *)
 
-let build_expected_arity env isevars isdep tomatchl =
+let build_expected_arity env evdref isdep tomatchl =
   let cook n = function
     | _,IsInd (_,IndType(indf,_)) ->
         let indf' = lift_inductive_family n indf in
@@ -1443,7 +1443,7 @@ let set_arity_signature dep n arsign tomatchl pred x =
   in
   decomp_block [] pred (tomatchl,arsign)
 
-let prepare_predicate_from_tycon loc dep env isevars tomatchs sign c =
+let prepare_predicate_from_tycon loc dep env evdref tomatchs sign c =
   let cook (n, l, env, signs) = function
     | c,IsInd (_,IndType(indf,realargs)) ->
 	let indf' = lift_inductive_family n indf in
@@ -1458,14 +1458,14 @@ let prepare_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 (Evd.evars_of !evdref) 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 (evars_of evdref) 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)
+      e_new_evar evdref env  ~src:(loc, Evd.CasesType)
+        (Retyping.get_type_of env (Evd.evars_of !evdref) c)
     else
       map_constr_with_full_binders push_rel build_skeleton env c 
   in
@@ -1530,11 +1530,11 @@ let extract_arity_signature env0 tomatchl tmsign =
     | _ -> assert false
   in List.rev (buildrec 0 (tomatchl,tmsign))
 
-let inh_conv_coerce_to_tycon loc env isevars j tycon =
+let inh_conv_coerce_to_tycon loc env evdref j tycon =
   match tycon with
     | Some p ->
-	let (evd',j) = Coercion.inh_conv_coerce_to loc env !isevars j p in
-          isevars := evd';
+	let (evd',j) = Coercion.inh_conv_coerce_to loc env !evdref j p in
+          evdref := evd';
           j
     | None -> j
 
@@ -1549,13 +1549,13 @@ let inh_conv_coerce_to_tycon loc env isevars j tycon =
  * A type constraint but no annotation case: it is assumed non dependent.
  *)
 
-let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
+let prepare_predicate loc typing_fun evdref env tomatchs sign tycon = function
   (* No type annotation *)
   | None ->
       (match tycon with
        | Some (None, t) ->
 	   let names,pred = 
-	     prepare_predicate_from_tycon loc false env isevars tomatchs sign t 
+	     prepare_predicate_from_tycon loc false env evdref tomatchs sign t 
 	   in Some (build_initial_predicate false names pred)
        | _ -> None)
 
@@ -1568,29 +1568,29 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
       let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in
       let _ = 
 	option_map (fun tycon -> 
-		      isevars := Coercion.inh_conv_coerces_to loc env !isevars predcclj.uj_val 
+		      evdref := Coercion.inh_conv_coerces_to loc env !evdref predcclj.uj_val 
 		      (lift_tycon_type (List.length arsign) tycon))
 	  tycon
       in
-      let predccl = (j_nf_isevar !isevars predcclj).uj_val in      
+      let predccl = (j_nf_isevar !evdref predcclj).uj_val in      
 	Some (build_initial_predicate true allnames predccl)
 
 (**************************************************************************)
 (* Main entry of the matching compilation                                 *)
   
-let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns)=
+let compile_cases loc (typing_fun, evdref) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns)=
   
   (* We build the matrix of patterns and right-hand-side *)
   let matx = matx_of_eqns env tomatchl eqns in
     
   (* We build the vector of terms to match consistently with the *)
   (* constructors found in patterns *)
-  let tomatchs = coerce_to_indtype typing_fun isevars env matx tomatchl in
+  let tomatchs = coerce_to_indtype typing_fun evdref env matx tomatchl in
     
   (* We build the elimination predicate if any and check its consistency *)
   (* with the type of arguments to match *)
   let tmsign = List.map snd tomatchl in
-  let pred = prepare_predicate loc typing_fun isevars env tomatchs tmsign tycon predopt in
+  let pred = prepare_predicate loc typing_fun evdref env tomatchs tmsign tycon predopt in
     
   (* We push the initial terms to match and push their alias to rhs' envs *)
   (* names of aliases will be recovered from patterns (hence Anonymous here) *)
@@ -1598,7 +1598,7 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e
     
   let pb =
     { env      = env;
-      isevars  = isevars;
+      evdref   = evdref;
       pred     = pred;
       tomatch  = initial_pushed;
       history  = start_history (List.length initial_pushed);
@@ -1609,6 +1609,6 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e
   let j = compile pb in
     (* We check for unused patterns *)
     List.iter (check_unused_pattern env) matx;
-    inh_conv_coerce_to_tycon loc env isevars j tycon
+    inh_conv_coerce_to_tycon loc env evdref j tycon
 end
   
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 374f11543..62e29dc06 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -25,38 +25,38 @@ open Termops
 module type S = sig
   (*s Coercions. *)
   
-  (* [inh_app_fun env isevars j] coerces [j] to a function; i.e. it
+  (* [inh_app_fun env evd j] coerces [j] to a function; i.e. it
      inserts a coercion into [j], if needed, in such a way it gets as
      type a product; it returns [j] if no coercion is applicable *)
   val inh_app_fun :
     env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment
     
-  (* [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it
+  (* [inh_coerce_to_sort env evd j] coerces [j] to a type; i.e. it
      inserts a coercion into [j], if needed, in such a way it gets as
      type a sort; it fails if no coercion is applicable *)
   val inh_coerce_to_sort : loc ->
     env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_type_judgment
 
-  (* [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it
+  (* [inh_coerce_to_base env evd j] coerces [j] to its base type; i.e. it
      inserts a coercion into [j], if needed, in such a way it gets as
      type its base type (the notion depends on the coercion system) *)
   val inh_coerce_to_base : loc ->
     env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment
     
-  (* [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type 
+  (* [inh_conv_coerce_to loc env evd j t] coerces [j] to an object of type 
      [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
      [j.uj_type] are convertible; it fails if no coercion is applicable *)
   val inh_conv_coerce_to : loc -> 
     env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment
     
 
-  (* [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
+  (* [inh_conv_coerces_to loc env evd t t'] checks if an object of type [t]
      is coercible to an object of type [t'] adding evar constraints if needed;
      it fails if no coercion exists *)
   val inh_conv_coerces_to : loc -> 
     env -> evar_defs -> types -> type_constraint_type -> evar_defs
 
-  (* [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases
+  (* [inh_pattern_coerce_to loc env evd pat ind1 ind2] coerces the Cases
      pattern [pat] typed in [ind1] into a pattern typed in [ind2];
      raises [Not_found] if no coercion found *)
   val inh_pattern_coerce_to :
@@ -72,8 +72,8 @@ module Default = struct
       | App (f,l) -> mkApp (whd_evar sigma f,l)
       | _ -> whd_evar sigma t
 
-  let class_of1 env isevars t =
-    let sigma = evars_of isevars in
+  let class_of1 env evd t =
+    let sigma = evars_of evd in
     class_of env sigma (whd_app_evar sigma t)
 
   (* Here, funj is a coercion therefore already typed in global context *)
@@ -122,47 +122,47 @@ module Default = struct
              (hj,typ_cl) p)
     with _ -> anomaly "apply_coercion"
 
-  let inh_app_fun env isevars j = 
-    let t = whd_betadeltaiota env (evars_of isevars) j.uj_type in
+  let inh_app_fun env evd j = 
+    let t = whd_betadeltaiota env (evars_of evd) j.uj_type in
       match kind_of_term t with
-	| Prod (_,_,_) -> (isevars,j)
+	| Prod (_,_,_) -> (evd,j)
 	| Evar ev ->
-	    let (isevars',t) = define_evar_as_arrow isevars ev in
-	      (isevars',{ uj_val = j.uj_val; uj_type = t })
+	    let (evd',t) = define_evar_as_arrow evd ev in
+	      (evd',{ uj_val = j.uj_val; uj_type = t })
 	| _ ->
        	    (try
- 	       let t,i1 = class_of1 env isevars j.uj_type in
+ 	       let t,i1 = class_of1 env evd j.uj_type in
       	       let p = lookup_path_to_fun_from i1 in
-		 (isevars,apply_coercion env p j t)
-	     with Not_found -> (isevars,j))
+		 (evd,apply_coercion env p j t)
+	     with Not_found -> (evd,j))
 
-  let inh_tosort_force loc env isevars j =
+  let inh_tosort_force loc env evd j =
     try
-      let t,i1 = class_of1 env isevars j.uj_type in
+      let t,i1 = class_of1 env evd j.uj_type in
       let p = lookup_path_to_sort_from i1 in
       let j1 = apply_coercion env p j t in 
-      let j2 = on_judgment_type (whd_evar (evars_of isevars)) j1 in
-        (isevars,type_judgment env j2)
+      let j2 = on_judgment_type (whd_evar (evars_of evd)) j1 in
+        (evd,type_judgment env j2)
     with Not_found ->
-      error_not_a_type_loc loc env (evars_of isevars) j
+      error_not_a_type_loc loc env (evars_of evd) j
 
-  let inh_coerce_to_sort loc env isevars j =
-    let typ = whd_betadeltaiota env (evars_of isevars) j.uj_type in
+  let inh_coerce_to_sort loc env evd j =
+    let typ = whd_betadeltaiota env (evars_of evd) 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) ->
-	    let (isevars',s) = define_evar_as_sort isevars ev in
-	      (isevars',{ utj_val = j.uj_val; utj_type = s })
+	| Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s })
+	| Evar ev when not (is_defined_evar evd ev) ->
+	    let (evd',s) = define_evar_as_sort evd ev in
+	      (evd',{ utj_val = j.uj_val; utj_type = s })
 	| _ ->
-	    inh_tosort_force loc env isevars j
+	    inh_tosort_force loc env evd j
 
-  let inh_coerce_to_base loc env isevars j = (isevars, j)
+  let inh_coerce_to_base loc env evd j = (evd, j)
 
-  let inh_coerce_to_fail env isevars c1 v t =
+  let inh_coerce_to_fail env evd c1 v t =
     let v', t' =
       try 
-	let t1,i1 = class_of1 env isevars c1 in
-	let t2,i2 = class_of1 env isevars t in
+	let t1,i1 = class_of1 env evd c1 in
+	let t2,i2 = class_of1 env evd t in
 	let p = lookup_path_between (i2,i1) in
 	  match v with
 	      Some v -> 
@@ -171,30 +171,30 @@ module Default = struct
 	    | None -> None, t
       with Not_found -> raise NoCoercion 
     in
-      try (the_conv_x_leq env t' c1 isevars, v', t')
+      try (the_conv_x_leq env t' c1 evd, v', t')
       with Reduction.NotConvertible -> raise NoCoercion
 
-  let rec inh_conv_coerce_to_fail loc env isevars v t c1 =
-    try (the_conv_x_leq env t c1 isevars, v, t)
+  let rec inh_conv_coerce_to_fail loc env evd v t c1 =
+    try (the_conv_x_leq env t c1 evd, v, t)
     with Reduction.NotConvertible ->
-    try inh_coerce_to_fail env isevars c1 v t
+    try inh_coerce_to_fail env evd c1 v t
     with NoCoercion ->
     match
-      kind_of_term (whd_betadeltaiota env (evars_of isevars) t),
-      kind_of_term (whd_betadeltaiota env (evars_of isevars) c1)
+      kind_of_term (whd_betadeltaiota env (evars_of evd) t),
+      kind_of_term (whd_betadeltaiota env (evars_of evd) c1)
     with
     | Prod (_,t1,t2), Prod (name,u1,u2) -> 
-	let v' = option_map (whd_betadeltaiota env (evars_of isevars)) v in
+	let v' = option_map (whd_betadeltaiota env (evars_of evd)) v in
 	let (evd',b) =
 	  match v' with 
 	  | Some v' ->
 	      (match kind_of_term v' with
 	       | Lambda (x,v1,v2) ->
 		   (* sous-typage non contravariant: pas de "leq v1 u1" *)
-		   (try the_conv_x env v1 u1 isevars, Some (x, v1, v2)
-		   with Reduction.NotConvertible -> (isevars, None))
-	       | _  -> (isevars, None))
-	  | None -> (isevars, None)
+		   (try the_conv_x env v1 u1 evd, Some (x, v1, v2)
+		   with Reduction.NotConvertible -> (evd, None))
+	       | _  -> (evd, None))
+	  | None -> (evd, None)
 	in
 	(match b with
 	 | Some (x, v1, v2) ->
@@ -213,7 +213,7 @@ module Default = struct
 	     in
 	     let env1 = push_rel (name,None,u1) env in
 	     let (evd', v1', t1') =
-	       inh_conv_coerce_to_fail loc env1 isevars
+	       inh_conv_coerce_to_fail loc env1 evd
 		 (Some (mkRel 1)) (lift 1 u1) (lift 1 t1)
 	     in
 	     let (evd'', v2', t2') = 
@@ -236,21 +236,21 @@ module Default = struct
     | _ -> raise NoCoercion
 
   (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
-  let inh_conv_coerce_to loc env isevars cj (n, t) =
+  let inh_conv_coerce_to loc env evd cj (n, t) =
     match n with
 	None ->
 	  let (evd', val', type') = 
 	    try 
-	      inh_conv_coerce_to_fail loc env isevars (Some cj.uj_val) cj.uj_type t
+	      inh_conv_coerce_to_fail loc env evd (Some cj.uj_val) cj.uj_type t
 	    with NoCoercion ->
-	      let sigma = evars_of isevars in
+	      let sigma = evars_of evd in
 		error_actual_type_loc loc env sigma cj t
 	  in
 	  let val' = match val' with Some v -> v | None -> assert(false) in
 	    (evd',{ uj_val = val'; uj_type = t })
-      | Some (init, cur) -> (isevars, cj)
+      | Some (init, cur) -> (evd, cj)
       
-    let inh_conv_coerces_to loc env (isevars : evar_defs) t (abs, t') = isevars
+    let inh_conv_coerces_to loc env (evd : evar_defs) t (abs, t') = evd
       (* Still problematic, as it changes unification 
       let nabsinit, nabs = 
 	match abs with
@@ -274,11 +274,11 @@ module Default = struct
 		  env', rng, lift nabs t'
 	      in
 		try 
-		  pi1 (inh_conv_coerce_to_fail loc env' isevars None t t')
+		  pi1 (inh_conv_coerce_to_fail loc env' evd None t t')
 		with NoCoercion ->
-		  isevars) (* Maybe not enough information to unify *)
-	      (*let sigma = evars_of isevars in
+		  evd) (* Maybe not enough information to unify *)
+	      (*let sigma = evars_of evd in
 		error_cannot_coerce env' sigma (t, t'))*)
-	    else isevars
-	with Invalid_argument _ -> isevars	  *)
+	    else evd
+	with Invalid_argument _ -> evd	  *)
 end
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 66270c2b3..b65ad37b1 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -67,30 +67,30 @@ let rec apprec_nobeta env sigma s =
 	     | NotReducible -> s)
     | _ -> s
 
-let evar_apprec_nobeta env isevars stack c =
+let evar_apprec_nobeta env evd stack c =
   let rec aux s =
-    let (t,stack as s') = apprec_nobeta env (evars_of isevars) s in
+    let (t,stack as s') = apprec_nobeta env (evars_of evd) s in
     match kind_of_term t with
-      | Evar (n,_ as ev) when Evd.is_defined (evars_of isevars) n ->
-	  aux (Evd.existential_value (evars_of isevars) ev, stack)
+      | Evar (evk,_ as ev) when Evd.is_defined (evars_of evd) evk ->
+	  aux (Evd.existential_value (evars_of evd) ev, stack)
       | _ -> (t, list_of_stack stack)
   in aux (c, append_stack (Array.of_list stack) empty_stack)
 *)
 
-let evar_apprec env isevars stack c =
-  let sigma = evars_of isevars in
+let evar_apprec env evd stack c =
+  let sigma = evars_of evd in
   let rec aux s =
     let (t,stack) = Reductionops.apprec env sigma s in
     match kind_of_term t with
-      | Evar (n,_ as ev) when Evd.is_defined sigma n ->
+      | Evar (evk,_ as ev) when Evd.is_defined sigma evk ->
 	  aux (Evd.existential_value sigma ev, stack)
       | _ -> (t, list_of_stack stack)
   in aux (c, append_stack_list stack empty_stack)
 
-let apprec_nohdbeta env isevars c =
+let apprec_nohdbeta env evd c =
   let (t,stack as s) = Reductionops.whd_stack c in
   match kind_of_term t with
-    | (Case _ | Fix _) -> evar_apprec env isevars [] c
+    | (Case _ | Fix _) -> evar_apprec env evd [] c
     | _ -> s
 
 (* [check_conv_record (t1,l1) (t2,l2)] tries to decompose the problem
@@ -131,46 +131,46 @@ let check_conv_record (t1,l1) (t2,l2) =
 (* Precondition: one of the terms of the pb is an uninstantiated evar,
  * possibly applied to arguments. *)
 
-let rec ise_try isevars = function
+let rec ise_try evd = function
     [] -> assert false
-  | [f] -> f isevars
+  | [f] -> f evd
   | f1::l ->
-      let (isevars',b) = f1 isevars in
-      if b then (isevars',b) else ise_try isevars l
+      let (evd',b) = f1 evd in
+      if b then (evd',b) else ise_try evd l
 
-let ise_and isevars l =
+let ise_and evd l =
   let rec ise_and i = function
       [] -> assert false
     | [f] -> f i
     | f1::l ->
         let (i',b) = f1 i in
-        if b then  ise_and i' l else (isevars,false) in
-  ise_and isevars l
+        if b then  ise_and i' l else (evd,false) in
+  ise_and evd l
 
-let ise_list2 isevars f l1 l2 =
+let ise_list2 evd f l1 l2 =
   let rec ise_list2 i l1 l2 =
     match l1,l2 with
         [], [] -> (i, true)
       | [x], [y] -> f i x y
       | x::l1, y::l2 ->
           let (i',b) = f i x y in
-          if b then ise_list2 i' l1 l2 else (isevars,false)
-      | _ -> (isevars, false) in
-  ise_list2 isevars l1 l2
+          if b then ise_list2 i' l1 l2 else (evd,false)
+      | _ -> (evd, false) in
+  ise_list2 evd l1 l2
 
-let ise_array2 isevars f v1 v2 =
+let ise_array2 evd f v1 v2 =
   let rec allrec i = function
     | -1 -> (i,true)
     | n ->
         let (i',b) = f i v1.(n) v2.(n) in
-        if b then allrec i' (n-1) else (isevars,false)
+        if b then allrec i' (n-1) else (evd,false)
   in 
   let lv1 = Array.length v1 in
-  if lv1 = Array.length v2 then allrec isevars (pred lv1) 
-  else (isevars,false)
+  if lv1 = Array.length v2 then allrec evd (pred lv1) 
+  else (evd,false)
 
-let rec evar_conv_x env isevars pbty term1 term2 = 
-  let sigma = evars_of isevars in
+let rec evar_conv_x env evd pbty term1 term2 = 
+  let sigma = evars_of evd in
   let term1 = whd_castappevar sigma term1 in
   let term2 = whd_castappevar sigma term2 in
 (*
@@ -181,19 +181,19 @@ let rec evar_conv_x env isevars pbty term1 term2 =
   (* Maybe convertible but since reducing can erase evars which [evar_apprec]
      could have found, we do it only if the terms are free of evar.
      Note: incomplete heuristic... *)
-  if is_ground_term isevars term1 && is_ground_term isevars term2 &
-     is_fconv pbty env (evars_of isevars) term1 term2 then
-      (isevars,true)
-  else if is_undefined_evar isevars term1 then
-    solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term1,term2)
-  else if is_undefined_evar isevars term2 then
-    solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term2,term1)
+  if is_ground_term evd term1 && is_ground_term evd term2 &
+     is_fconv pbty env (evars_of evd) term1 term2 then
+      (evd,true)
+  else if is_undefined_evar evd term1 then
+    solve_simple_eqn evar_conv_x env evd (pbty,destEvar term1,term2)
+  else if is_undefined_evar evd term2 then
+    solve_simple_eqn evar_conv_x env evd (pbty,destEvar term2,term1)
   else 
-    let (t1,l1) = apprec_nohdbeta env isevars term1 in
-    let (t2,l2) = apprec_nohdbeta env isevars term2 in
-    evar_eqappr_x env isevars pbty (t1,l1) (t2,l2)
+    let (t1,l1) = apprec_nohdbeta env evd term1 in
+    let (t2,l2) = apprec_nohdbeta env evd term2 in
+    evar_eqappr_x env evd pbty (t1,l1) (t2,l2)
 
-and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
+and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
   (* Evar must be undefined since we have whd_ised *)
   match (flex_kind_of_term term1 l1, flex_kind_of_term term2 l2) with
     | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
@@ -221,19 +221,19 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
                  (fun i -> evar_conv_x env i CONV) l1 l2)]
           else (i,false)
 	in 
-	ise_try isevars [f1; f2]
+	ise_try evd [f1; f2]
 
     | Flexible ev1, MaybeFlexible flex2 ->
 	let f1 i =
 	  if 
 	    is_unification_pattern_evar ev1 l1 & 
-	    not (occur_evar (fst ev1) (applist (term2,l2)))
+	    not (occur_evar (fst ev1) (applist appr2))
 	  then
 	    (* Miller-Pfenning's patterns unification *)
 	    (* Preserve generality (except that CCI has no eta-conversion) *)
-	    let t2 = nf_evar (evars_of isevars) (applist(term2,l2)) in
+	    let t2 = nf_evar (evars_of evd) (applist appr2) in
 	    let t2 = solve_pattern_eqn env l1 t2 in
-	    solve_simple_eqn evar_conv_x env isevars (pbty,ev1,t2)
+	    solve_simple_eqn evar_conv_x env evd (pbty,ev1,t2)
 	  else if
             List.length l1 <= List.length l2
 	  then
@@ -253,19 +253,19 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 		evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2)
 	    | None -> (i,false)
 	in 
-	ise_try isevars [f1; f4]
+	ise_try evd [f1; f4]
 
     | MaybeFlexible flex1, Flexible ev2 ->
 	let f1 i =
 	  if 
 	    is_unification_pattern_evar ev2 l2 & 
-	    not (occur_evar (fst ev2) (applist (term1,l1)))
+	    not (occur_evar (fst ev2) (applist appr1))
 	  then
 	    (* Miller-Pfenning's patterns unification *)
 	    (* Preserve generality (except that CCI has no eta-conversion) *)
-	    let t1 = nf_evar (evars_of isevars) (applist(term1,l1)) in
+	    let t1 = nf_evar (evars_of evd) (applist appr1) in
 	    let t1 = solve_pattern_eqn env l2 t1 in
-	    solve_simple_eqn evar_conv_x env isevars (pbty,ev2,t1)
+	    solve_simple_eqn evar_conv_x env evd (pbty,ev2,t1)
 	  else if
        	    List.length l2 <= List.length l1
 	  then
@@ -284,7 +284,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 		evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2
 	    | None -> (i,false)
 	in 
-	ise_try isevars [f1; f4]
+	ise_try evd [f1; f4]
 
     | MaybeFlexible flex1, MaybeFlexible flex2 ->
 	let f2 i =
@@ -313,36 +313,36 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 		      evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2
 		  | None -> (i,false)
 	in 
-	ise_try isevars [f2; f3; f4]
+	ise_try evd [f2; f3; f4]
 
     | Flexible ev1, Rigid _ ->
 	if 
 	  is_unification_pattern_evar ev1 l1 & 
-	  not (occur_evar (fst ev1) (applist (term2,l2)))
+	  not (occur_evar (fst ev1) (applist appr2))
 	then
 	  (* Miller-Pfenning's patterns unification *)
 	  (* Preserve generality (except that CCI has no eta-conversion) *)
-	  let t2 = nf_evar (evars_of isevars) (applist(term2,l2)) in
+	  let t2 = nf_evar (evars_of evd) (applist appr2) in
 	  let t2 = solve_pattern_eqn env l1 t2 in
-	  solve_simple_eqn evar_conv_x env isevars (pbty,ev1,t2)
+	  solve_simple_eqn evar_conv_x env evd (pbty,ev1,t2)
 	else
 	  (* Postpone the use of an heuristic *)
-	  add_conv_pb (pbty,env,applist(term1,l1),applist(term2,l2)) isevars,
+	  add_conv_pb (pbty,env,applist appr1,applist appr2) evd,
 	  true
 
     | Rigid _, Flexible ev2 ->
 	if 
 	  is_unification_pattern_evar ev2 l2 & 
-	  not (occur_evar (fst ev2) (applist (term1,l1)))
+	  not (occur_evar (fst ev2) (applist appr1))
 	then
 	  (* Miller-Pfenning's patterns unification *)
 	  (* Preserve generality (except that CCI has no eta-conversion) *)
-	  let t1 = nf_evar (evars_of isevars) (applist(term1,l1)) in
+	  let t1 = nf_evar (evars_of evd) (applist appr1) in
 	  let t1 = solve_pattern_eqn env l2 t1 in
-	  solve_simple_eqn evar_conv_x env isevars (pbty,ev2,t1)
+	  solve_simple_eqn evar_conv_x env evd (pbty,ev2,t1)
 	else
 	  (* Postpone the use of an heuristic *)
-	  add_conv_pb (pbty,env,applist(term1,l1),applist(term2,l2)) isevars,
+	  add_conv_pb (pbty,env,applist appr1,applist appr2) evd,
 	  true
 
     | MaybeFlexible flex1, Rigid _ ->
@@ -355,7 +355,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
  		evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2
 	    | None -> (i,false)
 	in 
-	ise_try isevars [f3; f4]
+	ise_try evd [f3; f4]
 	     
     | Rigid _ , MaybeFlexible flex2 -> 
 	let f3 i = 
@@ -367,19 +367,19 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
  		evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2)
 	    | None -> (i,false)
 	in 
-	ise_try isevars [f3; f4]
+	ise_try evd [f3; f4]
 
     | Rigid c1, Rigid c2 -> match kind_of_term c1, kind_of_term c2 with
 	  
-	| Cast (c1,_,_), _ -> evar_eqappr_x env isevars pbty (c1,l1) appr2
+	| Cast (c1,_,_), _ -> evar_eqappr_x env evd pbty (c1,l1) appr2
 
-	| _, Cast (c2,_,_) -> evar_eqappr_x env isevars pbty appr1 (c2,l2)
+	| _, Cast (c2,_,_) -> evar_eqappr_x env evd pbty appr1 (c2,l2)
 
 	| Sort s1, Sort s2 when l1=[] & l2=[] ->
-            (isevars,base_sort_cmp pbty s1 s2)
+            (evd,base_sort_cmp pbty s1 s2)
 
 	| Lambda (na,c1,c'1), Lambda (_,c2,c'2) when l1=[] & l2=[] -> 
-            ise_and isevars
+            ise_and evd
               [(fun i -> evar_conv_x env i CONV c1 c2);
                (fun i ->
                  let c = nf_evar (evars_of i) c1 in
@@ -400,18 +400,18 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
               and appr2 = evar_apprec env i l2 (subst1 b2 c'2)
 	      in evar_eqappr_x env i pbty appr1 appr2
 	    in 
-	    ise_try isevars [f1; f2]
+	    ise_try evd [f1; f2]
 
 	| LetIn (_,b1,_,c'1), _ ->(* On fait commuter les args avec le Let *)
-	     let appr1 = evar_apprec env isevars l1 (subst1 b1 c'1)
-             in evar_eqappr_x env isevars pbty appr1 appr2
+	     let appr1 = evar_apprec env evd l1 (subst1 b1 c'1)
+             in evar_eqappr_x env evd pbty appr1 appr2
 
 	| _, LetIn (_,b2,_,c'2) ->
-	    let appr2 = evar_apprec env isevars l2 (subst1 b2 c'2)
-            in evar_eqappr_x env isevars pbty appr1 appr2
+	    let appr2 = evar_apprec env evd l2 (subst1 b2 c'2)
+            in evar_eqappr_x env evd pbty appr1 appr2
 
 	| Prod (n,c1,c'1), Prod (_,c2,c'2) when l1=[] & l2=[] -> 
-            ise_and isevars
+            ise_and evd
               [(fun i -> evar_conv_x env i CONV c1 c2);
                (fun i ->
  	         let c = nf_evar (evars_of i) c1 in
@@ -419,16 +419,16 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 
 	| Ind sp1, Ind sp2 ->
 	    if sp1=sp2 then
-              ise_list2 isevars (fun i -> evar_conv_x env i CONV) l1 l2
-            else (isevars, false)
+              ise_list2 evd (fun i -> evar_conv_x env i CONV) l1 l2
+            else (evd, false)
 
 	| Construct sp1, Construct sp2 ->
 	    if sp1=sp2 then
-              ise_list2 isevars (fun i -> evar_conv_x env i CONV) l1 l2
-            else (isevars, false)
+              ise_list2 evd (fun i -> evar_conv_x env i CONV) l1 l2
+            else (evd, false)
 
 	| Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
-            ise_and isevars
+            ise_and evd
               [(fun i -> evar_conv_x env i CONV p1 p2);
                (fun i -> evar_conv_x env i CONV c1 c2);
 	       (fun i -> ise_array2 i
@@ -437,7 +437,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 
 	| Fix (li1,(_,tys1,bds1 as recdef1)), Fix (li2,(_,tys2,bds2)) ->
             if li1=li2 then
-              ise_and isevars
+              ise_and evd
                 [(fun i -> ise_array2 i
                     (fun i -> evar_conv_x env i CONV) tys1 tys2);
                  (fun i -> ise_array2 i
@@ -445,10 +445,10 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 		     bds1 bds2);
 	         (fun i -> ise_list2 i
                      (fun i -> evar_conv_x env i CONV) l1 l2)]
-	    else (isevars,false)
+	    else (evd,false)
 	| CoFix (i1,(_,tys1,bds1 as recdef1)), CoFix (i2,(_,tys2,bds2)) ->
             if i1=i2  then
-              ise_and isevars
+              ise_and evd
                 [(fun i -> ise_array2 i
                     (fun i -> evar_conv_x env i CONV) tys1 tys2);
                  (fun i -> ise_array2 i
@@ -456,30 +456,30 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 		     bds1 bds2);
                  (fun i -> ise_list2 i
                      (fun i -> evar_conv_x env i CONV) l1 l2)]
-            else (isevars,false)
+            else (evd,false)
 
-	| (Meta _ | Lambda _), _ -> (isevars,false)
-	| _, (Meta _ | Lambda _) -> (isevars,false)
+	| (Meta _ | Lambda _), _ -> (evd,false)
+	| _, (Meta _ | Lambda _) -> (evd,false)
 
-	| (Ind _ | Construct _ | Sort _ | Prod _), _ -> (isevars,false)
-	| _, (Ind _ | Construct _ | Sort _ | Prod _) -> (isevars,false)
+	| (Ind _ | Construct _ | Sort _ | Prod _), _ -> (evd,false)
+	| _, (Ind _ | Construct _ | Sort _ | Prod _) -> (evd,false)
 
 	| (App _ | Case _ | Fix _ | CoFix _), 
-	  (App _ | Case _ | Fix _ | CoFix _) -> (isevars,false)
+	  (App _ | Case _ | Fix _ | CoFix _) -> (evd,false)
 
 	| (Rel _ | Var _ | Const _ | Evar _), _ -> assert false
 	| _, (Rel _ | Var _ | Const _ | Evar _) -> assert false
 
-and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) = 
-  let (isevars',ks) =
+and conv_record env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1) = 
+  let (evd',ks) =
     List.fold_left
       (fun (i,ks) b ->
 	 let dloc = (dummy_loc,InternalHole) in
          let (i',ev) = new_evar i env ~src:dloc (substl ks b) in
 	 (i', ev :: ks))
-      (isevars,[]) bs
+      (evd,[]) bs
   in
-  ise_and isevars'
+  ise_and evd'
     [(fun i ->
       ise_list2 i
         (fun i u1 u -> evar_conv_x env i CONV u1 (substl ks u))
@@ -491,11 +491,11 @@ and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) =
      (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) ts ts1);
      (fun i -> evar_conv_x env i CONV c1 (applist (c,(List.rev ks))))]
 
-let first_order_unification env isevars pbty (term1,l1) (term2,l2) =
+let first_order_unification env evd pbty (term1,l1) (term2,l2) =
   match kind_of_term term1, kind_of_term term2 with
     | Evar ev1,_ when List.length l1 <= List.length l2 ->
 	let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
-	ise_and isevars
+	ise_and evd
           (* First compare extra args for better failure message *)
         [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest2 l1);
 	(fun i ->
@@ -507,7 +507,7 @@ let first_order_unification env isevars pbty (term1,l1) (term2,l2) =
 	    solve_simple_eqn evar_conv_x env i (pbty,ev1,t2))]
     | _,Evar ev2 when List.length l2 <= List.length l1 ->
 	let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
-	ise_and isevars
+	ise_and evd
           (* First compare extra args for better failure message *)
         [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest1 l2);
 	(fun i ->
@@ -519,37 +519,37 @@ let first_order_unification env isevars pbty (term1,l1) (term2,l2) =
 	    solve_simple_eqn evar_conv_x env i (pbty,ev2,t1))]
     | _ -> 
 	(* Some head evar have been instantiated *)
-	evar_conv_x env isevars pbty (applist(term1,l1)) (applist(term2,l2))
+	evar_conv_x env evd pbty (applist(term1,l1)) (applist(term2,l2))
 
-let consider_remaining_unif_problems env isevars =
-  let (isevars,pbs) = get_conv_pbs isevars (fun _ -> true) in
+let consider_remaining_unif_problems env evd =
+  let (evd,pbs) = get_conv_pbs evd (fun _ -> true) in
   List.fold_left
-    (fun (isevars,b as p) (pbty,env,t1,t2) ->
-      if b then first_order_unification env isevars pbty 
-	(apprec_nohdbeta env isevars (whd_castappevar (evars_of isevars) t1))
-	(apprec_nohdbeta env isevars (whd_castappevar (evars_of isevars) t2))
+    (fun (evd,b as p) (pbty,env,t1,t2) ->
+      if b then first_order_unification env evd pbty 
+	(apprec_nohdbeta env evd (whd_castappevar (evars_of evd) t1))
+	(apprec_nohdbeta env evd (whd_castappevar (evars_of evd) t2))
       else p)
-    (isevars,true)
+    (evd,true)
     pbs
 
 (* Main entry points *)
 
-let the_conv_x     env t1 t2 isevars =
-  match evar_conv_x env isevars CONV  t1 t2 with
+let the_conv_x     env t1 t2 evd =
+  match evar_conv_x env evd CONV  t1 t2 with
       (evd',true) -> evd'
     | _ -> raise Reduction.NotConvertible
 
-let the_conv_x_leq env t1 t2 isevars =
-  match evar_conv_x env isevars CUMUL t1 t2 with
+let the_conv_x_leq env t1 t2 evd =
+  match evar_conv_x env evd CUMUL t1 t2 with
       (evd', true) -> evd'
     | _ -> raise Reduction.NotConvertible
  
-let e_conv env isevars t1 t2 =
-  match evar_conv_x env !isevars CONV t1 t2 with
-      (evd',true) -> isevars := evd'; true
+let e_conv env evd t1 t2 =
+  match evar_conv_x env !evd CONV t1 t2 with
+      (evd',true) -> evd := evd'; true
     | _ -> false
 
-let e_cumul env isevars t1 t2 =
-  match evar_conv_x env !isevars CUMUL t1 t2 with
-      (evd',true) -> isevars := evd'; true
+let e_cumul env evd t1 t2 =
+  match evar_conv_x env !evd CUMUL t1 t2 with
+      (evd',true) -> evd := evd'; true
     | _ -> false
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 87bbc5de2..28473962a 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -29,10 +29,10 @@ exception Uninstantiated_evar of existential_key
 
 let rec whd_ise sigma c =
   match kind_of_term c with
-    | Evar (ev,args) when Evd.mem sigma ev ->
-	if Evd.is_defined sigma ev then
-          whd_ise sigma (existential_value sigma (ev,args))
-	else raise (Uninstantiated_evar ev)
+    | Evar (evk,args as ev) when Evd.mem sigma evk ->
+	if Evd.is_defined sigma evk then
+          whd_ise sigma (existential_value sigma ev)
+	else raise (Uninstantiated_evar evk)
   | _ -> c
 
 
@@ -40,8 +40,8 @@ let rec whd_ise sigma c =
 let whd_castappevar_stack sigma c = 
   let rec whrec (c, l as s) =
     match kind_of_term c with
-      | Evar (ev,args) when Evd.mem sigma ev & Evd.is_defined sigma ev -> 
-	  whrec (existential_value sigma (ev,args), l)
+      | Evar (evk,args as ev) when Evd.mem sigma evk & Evd.is_defined sigma evk
+	  -> whrec (existential_value sigma ev, l)
       | Cast (c,_,_) -> whrec (c, l)
       | App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
       | _ -> s
@@ -64,13 +64,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 isevars = Evd.evars_reset_evd (nf_evars (Evd.evars_of isevars)) isevars
+let nf_evar_defs evd = Evd.evars_reset_evd (nf_evars (Evd.evars_of evd)) evd
 
-let nf_isevar isevars = nf_evar (Evd.evars_of isevars)
-let j_nf_isevar isevars = j_nf_evar (Evd.evars_of isevars)
-let jl_nf_isevar isevars = jl_nf_evar (Evd.evars_of isevars)
-let jv_nf_isevar isevars = jv_nf_evar (Evd.evars_of isevars)
-let tj_nf_isevar isevars = tj_nf_evar (Evd.evars_of isevars)
+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)
 
 (**********************)
 (* Creating new metas *)
@@ -86,8 +86,8 @@ let mk_new_meta () = mkMeta(new_meta())
 let collect_evars emap c =
   let rec collrec acc c =
     match kind_of_term c with
-      | Evar (k,_) ->
-	  if Evd.mem emap k & not (Evd.is_defined emap k) then k::acc
+      | Evar (evk,_) ->
+	  if Evd.mem emap evk & not (Evd.is_defined emap evk) then evk::acc
 	  else (* No recursion on the evar instantiation *) acc
       | _         ->
 	  fold_constr collrec acc c in
@@ -112,7 +112,7 @@ let evars_to_metas sigma (emap, c) =
     mkCast (mkMeta n, DEFAULTcast, ty) in
   let rec replace c =
     match kind_of_term c with
-        Evar (k,_ as ev) when Evd.mem emap' k -> change_exist ev
+      | Evar (evk,_ as ev) when Evd.mem emap' evk -> change_exist ev
       | _ -> map_constr replace c in
   (sigma', replace c)
 
@@ -121,9 +121,9 @@ let evars_to_metas sigma (emap, c) =
 let non_instantiated sigma = 
   let listev = to_list sigma in
   List.fold_left 
-    (fun l (ev,evd) -> 
-       if evd.evar_body = Evar_empty then 
-	 ((ev,nf_evar_info sigma evd)::l) else l)
+    (fun l (ev,evi) -> 
+       if evi.evar_body = Evar_empty then 
+	 ((ev,nf_evar_info sigma evi)::l) else l)
     [] listev
 
 (**********************)
@@ -144,9 +144,9 @@ let new_evar_instance sign evd typ ?(src=(dummy_loc,InternalHole)) instance =
     (let ctxt = named_context_of_val sign in
      List.length instance = named_context_length ctxt &
      list_distinct (ids_of_named_context ctxt));
-  let newev = new_untyped_evar() in
-  let evd = evar_declare sign newev typ ~src:src evd in
-  (evd,mkEvar (newev,Array.of_list instance))
+  let newevk = new_untyped_evar() in
+  let evd = evar_declare sign newevk typ ~src:src evd in
+  (evd,mkEvar (newevk,Array.of_list instance))
 
 (* Knowing that [Gamma |- ev : T] and that [ev] is applied to [args],
  * [make_projectable_subst ev args] builds the substitution [Gamma:=args].
@@ -231,13 +231,13 @@ let push_rel_context_to_named_context env typ =
 
 let new_evar evd env ?(src=(dummy_loc,InternalHole)) typ =
   let sign,typ',instance = push_rel_context_to_named_context env typ in
-    new_evar_instance sign evd typ' ~src:src instance
+  new_evar_instance sign evd typ' ~src:src instance
 
   (* The same using side-effect *)
-let e_new_evar evd env ?(src=(dummy_loc,InternalHole)) ty =
-  let (evd',ev) = new_evar !evd env ~src:src ty in
-    evd := evd';
-    ev
+let e_new_evar evdref env ?(src=(dummy_loc,InternalHole)) ty =
+  let (evd',ev) = new_evar !evdref env ~src:src ty in
+  evdref := evd';
+  ev
 
 (*------------------------------------*
  * operations on the evar constraints *
@@ -267,12 +267,12 @@ let evar_well_typed_body evd ev evi body =
 
 let strict_inverse = false
 
-let inverse_instance env isevars ev evi inst rhs =
-  let subst = make_projectable_subst (evars_of isevars) evi inst in
+let inverse_instance env evd ev evi inst rhs =
+  let subst = make_projectable_subst (evars_of evd) evi inst in
   let subst = List.map (fun (x,(_,y)) -> (y,mkVar x)) subst in
-  let evd = ref isevars in
+  let evdref = ref evd in
   let error () = 
-    error_not_clean env (evars_of !evd) ev rhs (evar_source ev !evd) in
+    error_not_clean env (evars_of !evdref) ev rhs (evar_source ev !evdref) in
   let rec subs rigid k t =
     match kind_of_term t with
       | Rel i ->
@@ -294,15 +294,15 @@ let inverse_instance env isevars ev evi inst rhs =
              then
                failwith "cannot solve pb yet"
              else t)
-      | Evar (ev,args) ->
-          if Evd.is_defined_evar !evd (ev,args) then
-            subs rigid k (existential_value (evars_of !evd) (ev,args))
+      | Evar (evk,args as ev) ->
+          if Evd.is_defined_evar !evdref ev then
+            subs rigid k (existential_value (evars_of !evdref) ev)
           else
 	    let args' = Array.map (subs false k) args in
-	    mkEvar (ev,args')
+	    mkEvar (evk,args')
       | _ -> map_constr_with_binders succ (subs rigid) k t in
-  let body = subs true 0 (nf_evar (evars_of isevars) rhs) in
-  (!evd,body)
+  let body = subs true 0 (nf_evar (evars_of evd) rhs) in
+  (!evdref,body)
 
 
 let is_defined_equation env evd (ev,inst) rhs =
@@ -328,9 +328,9 @@ let is_defined_equation env evd (ev,inst) rhs =
  * We create "env' |- ev' : T" for some env' <= env and define ev:=ev'
 *)
 
-let do_restrict_hyps env k evd ev args =
+let do_restrict_hyps env k evdref ev args =
   let args = Array.to_list args in
-  let evi = Evd.find (evars_of !evd) ev in
+  let evi = Evd.find (evars_of !evdref) ev in
   let hyps = evar_context evi in
   let (hyps',ncargs) = list_filter2 (fun _ a -> closedn k a) (hyps,args) in
     (* No care is taken in case the evar type uses vars filtered out!
@@ -342,14 +342,15 @@ let do_restrict_hyps env k evd ev args =
        restriction raise no de Bruijn reallocation problem *)
   let env' =
     Sign.fold_named_context push_named hyps' ~init:(reset_context env) in
-  let nc = e_new_evar evd env' ~src:(evar_source ev !evd) evi.evar_concl in
-    evd := Evd.evar_define ev nc !evd;
-    let (evn,_) = destEvar nc in
-      mkEvar(evn,Array.of_list ncargs)
+  let nc =
+    e_new_evar evdref env' ~src:(evar_source ev !evdref) evi.evar_concl in
+  evdref := Evd.evar_define ev nc !evdref;
+  let (evk,_) = destEvar nc in
+  mkEvar(evk,Array.of_list ncargs)
 
 exception Dependency_error of identifier
-	
-let rec check_and_clear_in_constr evd c ids =
+
+let rec check_and_clear_in_constr evdref c ids =
   (* returns a new constr where all the evars have been 'cleaned'
      (ie the hypotheses ids have been removed from the contexts of
      evars *)
@@ -364,19 +365,19 @@ let rec check_and_clear_in_constr evd c ids =
 	    List.iter check vars; c
       | Var id' ->  
 	  check id'; mkVar id'
-      | Evar (e,l) -> 
-	  if Evd.is_defined_evar !evd (e,l) then
-	    (* If e is already defined we replace it by its definition *)
-	    let nc = nf_evar (evars_of !evd) c in 
-	      (check_and_clear_in_constr evd nc ids)
+      | 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 = nf_evar (evars_of !evdref) c in 
+	      (check_and_clear_in_constr evdref nc ids)
 	  else
 	    (* We check for dependencies to elements of ids in the
 	       evar_info corresponding to e and in the instance of
 	       arguments. Concurrently, we build a new evar
 	       corresponding to e where hypotheses of ids have been
 	       removed *)
-	    let evi = Evd.find (evars_of !evd) e in
-	    let nconcl = check_and_clear_in_constr evd (evar_concl evi) ids in
+	    let evi = Evd.find (evars_of !evdref) evk in
+	    let nconcl = check_and_clear_in_constr evdref (evar_concl evi) ids in
 	    let (nhyps,nargs) = 
 	      List.fold_right2 
 		(fun (id,ob,c) i (hy,ar) ->
@@ -386,24 +387,24 @@ let rec check_and_clear_in_constr evd c ids =
 		    let d' = (id,
 			     (match ob with 
 				 None -> None
-			       | Some b -> Some (check_and_clear_in_constr evd b ids)),
-			     check_and_clear_in_constr evd c ids) in
-		    let i' = check_and_clear_in_constr evd i ids in
+			       | Some b -> Some (check_and_clear_in_constr evdref b ids)),
+			     check_and_clear_in_constr evdref c ids) in
+		    let i' = check_and_clear_in_constr evdref i ids in
 		      (d'::hy, i'::ar)
 		) 	      
 		(evar_context evi) (Array.to_list l) ([],[]) in
 	    let env = Sign.fold_named_context push_named nhyps ~init:(empty_env) in
-	    let ev'= e_new_evar evd env ~src:(evar_source e !evd) nconcl in
-	      evd := Evd.evar_define e ev' !evd;
-	      let (e',_) = destEvar ev' in
-		mkEvar(e', Array.of_list nargs)
-      | _ -> map_constr (fun c -> check_and_clear_in_constr evd c ids) c
+	    let ev'= e_new_evar evdref env ~src:(evar_source evk !evdref) nconcl in
+	      evdref := Evd.evar_define evk ev' !evdref;
+	      let (evk',_) = destEvar ev' in
+		mkEvar(evk', Array.of_list nargs)
+      | _ -> map_constr (fun c -> check_and_clear_in_constr evdref c ids) c
 
-and clear_hyps_in_evi evd evi ids =
+and clear_hyps_in_evi evdref evi ids =
   (* clear_evar_hyps erases hypotheses ids in evi, checking if some
      hypothesis does not depend on a element of ids, and erases ids in
      the contexts of the evars occuring in evi *)
-  let nconcl = try check_and_clear_in_constr evd (evar_concl evi) ids 
+  let nconcl = try check_and_clear_in_constr evdref (evar_concl evi) ids 
     with Dependency_error id' -> error (string_of_id id' ^ " is used in conclusion") in
   let (nhyps,_) = 
     let check_context (id,ob,c) = 
@@ -411,8 +412,8 @@ and clear_hyps_in_evi evd evi ids =
 	(id,
 	(match ob with 
 	    None -> None
-	  | Some b -> Some (check_and_clear_in_constr evd b ids)),
-	check_and_clear_in_constr evd c ids)
+	  | Some b -> Some (check_and_clear_in_constr evdref b ids)),
+	check_and_clear_in_constr evdref c ids)
       with Dependency_error id' -> error (string_of_id id' ^ " is used in hypothesis "
 					   ^ string_of_id id) 
     in
@@ -466,8 +467,8 @@ let rec find_projectable_vars env sigma y subst =
   let is_projectable (id,(idc,y')) =
     if is_conv env sigma y y' then (idc,(y'=y,(id,ProjectVar)))
     else if isEvar y' then
-      let (ev,argsv as t) = destEvar y' in
-      let evi = Evd.find sigma ev in
+      let (evk,argsv as t) = destEvar y' in
+      let evi = Evd.find sigma evk in
       let subst = make_projectable_subst sigma evi argsv in
       let l = find_projectable_vars env sigma y subst in
       if l <> [] then (idc,(true,(id,ProjectEvar (t,evi,l))))
@@ -503,39 +504,39 @@ let rec find_projectable_vars env sigma y subst =
 
 exception NotClean of constr
 
-let rec real_clean env isevars ev subst rhs =
-  let evd = ref isevars in
+let rec real_clean env evd ev subst rhs =
+  let evdref = ref evd in
   let rec subs rigid k t =
     match kind_of_term t with
       | Rel i ->
  	 if i<=k then t
  	 else
 	   (* Flex/Rel problem: unifiable iff Rel projectable from ev subst *)
-	   project rigid env evd (mkRel (i-k)) subst
-      | Evar (ev,args) ->
-          if Evd.is_defined_evar !evd (ev,args) then
-            subs rigid k (existential_value (evars_of !evd) (ev,args))
+	   project rigid env evdref (mkRel (i-k)) subst
+      | Evar (evk,args as ev) ->
+          if Evd.is_defined_evar !evdref ev then
+            subs rigid k (existential_value (evars_of !evdref) ev)
           else
 	    (* Flex/Flex problem: restriction to a common scope *)
 	    let args' = Array.map (subs false k) args in
 	    if need_restriction k args' then
-              do_restrict_hyps (reset_context env) k evd ev args'
+              do_restrict_hyps (reset_context env) k evdref evk args'
 	    else
-	      mkEvar (ev,args')
+	      mkEvar (evk,args')
       | Var id ->
 	  (* Flex/Var problem: unifiable iff Var projectable from ev subst *)
-	  project rigid env evd t subst
+	  project rigid env evdref t subst
       | _ ->
 	  (* Flex/Rigid problem (or assimilated if not normal): we "imitate" *)
 	  map_constr_with_binders succ (subs rigid) k t
   in
-  let rhs = nf_evar (evars_of isevars) rhs in
+  let rhs = nf_evar (evars_of evd) rhs in
   let rhs = whd_beta rhs (* heuristic *) in
   let body = 
     try subs true 0 rhs
     with NotClean t -> 
-      error_not_clean env (evars_of !evd) ev t (evar_source ev !evd) in
-  (!evd,body)
+      error_not_clean env (evars_of !evdref) ev t (evar_source ev !evdref) in
+  (!evdref,body)
 
 (* Assume a set of solutions to the following two kinds of problems:
  *
@@ -550,16 +551,17 @@ let rec real_clean env isevars ev subst rhs =
  * the second kind of problem).
  *)
 
-and project rigid env isevars t subst =
+and project rigid env evdref t subst =
   let rec aux = function
   | [] -> raise Not_found
-  | (id,_)::_::_ ->
+  | (id,p)::_::_ ->
+      (* warning "More than one possible projection"; Pp.flush_all(); *)
       if rigid then raise Not_found else (* Irreversible choice *) mkVar id
   | [id,ProjectVar] -> mkVar id
-  | [id,ProjectEvar ((ev,argsv),evi,sols)] ->
-      isevars := Evd.evar_define ev (aux sols) !isevars;
-      let ty = Retyping.get_type_of env (evars_of !isevars) t in
-      let ty = whd_betadeltaiota env (evars_of !isevars) ty in
+  | [id,ProjectEvar ((evk,argsv),evi,sols)] ->
+      evdref := Evd.evar_define evk (aux sols) !evdref;
+      let ty = Retyping.get_type_of env (evars_of !evdref) t in
+      let ty = whd_betadeltaiota env (evars_of !evdref) ty in
       if not (isSort ty) & isEvar evi.evar_concl then
 	begin
 	  (* Don't try to instantiate if a sort because if evar_concl is an
@@ -568,10 +570,10 @@ and project rigid env isevars t subst =
              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
-	  isevars := fst (evar_define env (destEvar ty') ty !isevars)
+	  evdref := fst (evar_define env (destEvar ty') ty !evdref)
 	end;
       mkVar id in
-  try aux (List.rev (find_projectable_vars env (evars_of !isevars) t subst))
+  try aux (List.rev (find_projectable_vars env (evars_of !evdref) t subst))
   with Not_found -> if not rigid then t else raise (NotClean t)
 
 (* [evar_define] solves the problem "?ev[args] = rhs" when "?ev" is an 
@@ -582,13 +584,13 @@ and project rigid env isevars t subst =
  *)
 
 (* env needed for error messages... *)
-and evar_define env (ev,argsv) rhs isevars =
+and evar_define env (ev,argsv) rhs evd =
   if occur_evar ev rhs
-  then error_occur_check env (evars_of isevars) ev rhs;
-  let evi = Evd.find (evars_of isevars) ev in
+  then error_occur_check env (evars_of evd) ev rhs;
+  let evi = Evd.find (evars_of evd) ev in
   (* the bindings to invert *)
-  let subst = make_projectable_subst (evars_of isevars) evi argsv in
-  let (isevars',body) = real_clean env isevars ev subst rhs in
+  let subst = make_projectable_subst (evars_of evd) evi argsv in
+  let (evd',body) = real_clean env evd ev subst rhs in
   if occur_meta body then error "Meta cannot occur in evar body"
   else
     (* needed only if an inferred type *)
@@ -601,16 +603,16 @@ and evar_define env (ev,argsv) rhs isevars =
       try
         let env = evar_env evi in
         let ty = evi.evar_concl in
-        Typing.check env (evars_of isevars') body ty
+        Typing.check env (evars_of evd') body ty
       with e ->
         pperrnl
           (str "Ill-typed evar instantiation: " ++ fnl() ++
-           pr_evar_defs isevars' ++ fnl() ++
+           pr_evar_defs evd' ++ fnl() ++
            str "----> " ++ int ev ++ str " := " ++
            print_constr body);
         raise e in*)
-    let isevars'' = Evd.evar_define ev body isevars' in
-    isevars'',[ev]
+    let evd'' = Evd.evar_define ev body evd' in
+    evd'',[ev]
 
 
 
@@ -618,16 +620,16 @@ and evar_define env (ev,argsv) rhs isevars =
 (* Auxiliary functions for the conversion algorithms modulo evars
  *)
 
-let has_undefined_evars isevars t = 
-  try let _ = local_strong (whd_ise (evars_of isevars)) t in false
+let has_undefined_evars evd t = 
+  try let _ = local_strong (whd_ise (evars_of evd)) t in false
   with Uninstantiated_evar _ -> true
 
-let is_ground_term isevars t =
-  not (has_undefined_evars isevars t)
+let is_ground_term evd t =
+  not (has_undefined_evars evd t)
 
-let head_is_evar isevars = 
+let head_is_evar evd = 
   let rec hrec k = match kind_of_term k with
-    | Evar n   -> not (Evd.is_defined_evar isevars n)
+    | Evar ev   -> not (Evd.is_defined_evar evd ev)
     | App (f,_) -> hrec f
     | Cast (c,_,_) -> hrec c
     | _ -> false
@@ -640,16 +642,16 @@ let rec is_eliminator c = match kind_of_term c with
   | Cast (c,_,_) -> is_eliminator c
   | _ -> false
 
-let head_is_embedded_evar isevars c =
-  (head_is_evar isevars c) & (is_eliminator c)
+let head_is_embedded_evar evd c =
+  (head_is_evar evd c) & (is_eliminator c)
 
 let head_evar = 
   let rec hrec c = match kind_of_term c with
-    | Evar (ev,_)       -> ev
+    | Evar (evk,_)   -> evk
     | Case (_,_,c,_) -> hrec c
-    | App (c,_)        -> hrec c
-    | Cast (c,_,_)        -> hrec c
-    | _                   -> failwith "headconstant"
+    | App (c,_)      -> hrec c
+    | Cast (c,_,_)   -> hrec c
+    | _              -> failwith "headconstant"
   in 
   hrec 
 
@@ -718,25 +720,25 @@ let status_changed lev (pbty,_,t1,t2) =
  * that don't unify are discarded (i.e. ?i is redefined so that it does not
  * depend on these args). *)
 
-let solve_refl conv_algo env isevars ev argsv1 argsv2 =
-  if argsv1 = argsv2 then (isevars,[]) else
-  let evd = Evd.find (evars_of isevars) ev in
-  let hyps = evar_context evd in
-  let (isevars',_,rsign) = 
+let solve_refl conv_algo env evd ev argsv1 argsv2 =
+  if argsv1 = argsv2 then (evd,[]) else
+  let evi = Evd.find (evars_of evd) ev in
+  let hyps = evar_context evi in
+  let (evd',_,rsign) = 
     array_fold_left2
-      (fun (isevars,sgn,rsgn) a1 a2 ->
-        let (isevars',b) = conv_algo env isevars Reduction.CONV a1 a2 in
+      (fun (evd,sgn,rsgn) a1 a2 ->
+        let (evd',b) = conv_algo env evd Reduction.CONV a1 a2 in
 	 if b then 
-	   (isevars',List.tl sgn, add_named_decl (List.hd sgn) rsgn)
+	   (evd',List.tl sgn, add_named_decl (List.hd sgn) rsgn)
 	 else 
-	   (isevars,List.tl  sgn, rsgn))
-      (isevars,hyps,[]) argsv1 argsv2 
+	   (evd,List.tl  sgn, rsgn))
+      (evd,hyps,[]) argsv1 argsv2 
   in
   let nsign = List.rev rsign in
   let (evd',newev) =
     let env =
       Sign.fold_named_context push_named nsign ~init:(reset_context env) in
-    new_evar isevars env ~src:(evar_source ev isevars) evd.evar_concl in
+    new_evar evd env ~src:(evar_source ev evd) evi.evar_concl in
   let evd'' = Evd.evar_define ev newev evd' in
   evd'', [ev]
 
@@ -747,44 +749,44 @@ let solve_refl conv_algo env isevars ev argsv1 argsv2 =
  * if the problem couldn't be solved. *)
 
 (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *)
-let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) =
+let solve_simple_eqn conv_algo env evd (pbty,(evk1,args1 as ev1),t2) =
   try
-    let t2 = nf_evar (evars_of isevars) t2 in
-    let (isevars,lsp) = match kind_of_term t2 with
-      | Evar (n2,args2 as ev2) ->
-	  if n1 = n2 then
-	    solve_refl conv_algo env isevars n1 args1 args2
+    let t2 = nf_evar (evars_of evd) t2 in
+    let (evd,lsp) = match kind_of_term t2 with
+      | Evar (evk2,args2 as ev2) ->
+	  if evk1 = evk2 then
+	    solve_refl conv_algo env evd evk1 args1 args2
 	  else
-            (try evar_define env ev1 t2 isevars
+            (try evar_define env ev1 t2 evd
             with e when precatchable_exception e ->
-              evar_define env ev2 (mkEvar ev1) isevars)
+              evar_define env ev2 (mkEvar ev1) evd)
 (*	    if Array.length args1 < Array.length args2 then
-	      evar_define env ev2 (mkEvar ev1) isevars
+	      evar_define env ev2 (mkEvar ev1) evd
 	    else 
-	      evar_define env ev1 t2 isevars*)
+	      evar_define env ev1 t2 evd*)
       | _ ->
-	  evar_define env ev1 t2 isevars in
-    let (isevars,pbs) = get_conv_pbs isevars (status_changed lsp) in
+	  evar_define env ev1 t2 evd in
+    let (evd,pbs) = get_conv_pbs evd (status_changed lsp) in
     List.fold_left
-      (fun (isevars,b as p) (pbty,env,t1,t2) ->
-	if b then conv_algo env isevars pbty t1 t2 else p) (isevars,true)
+      (fun (evd,b as p) (pbty,env,t1,t2) ->
+	if b then conv_algo env evd pbty t1 t2 else p) (evd,true)
       pbs
   with e when precatchable_exception e ->
-    (isevars,false)
+    (evd,false)
 
 
 (* [check_evars] fails if some unresolved evar remains *)
 (* it assumes that the defined existentials have already been substituted *)
 
-let check_evars env initial_sigma isevars c =
-  let sigma = evars_of isevars in
+let check_evars env initial_sigma evd c =
+  let sigma = evars_of evd in
   let c = nf_evar sigma c in
   let rec proc_rec c =
     match kind_of_term c with
-      | Evar (ev,args) ->
-          assert (Evd.mem sigma ev);
-	  if not (Evd.mem initial_sigma ev) then
-            let (loc,k) = evar_source ev isevars in
+      | Evar (evk,args) ->
+          assert (Evd.mem sigma evk);
+	  if not (Evd.mem initial_sigma evk) then
+            let (loc,k) = evar_source evk evd in
 	    error_unsolvable_implicit loc env sigma k
       | _ -> iter_constr proc_rec c
   in proc_rec c
@@ -857,9 +859,9 @@ let define_evar_as_arrow evd (ev,args) =
 let define_evar_as_lambda evd (ev,args) =
   define_evar_as_abstraction (fun t -> mkLambda t) evd (ev,args)
 
-let define_evar_as_sort isevars (ev,args) =
+let define_evar_as_sort evd (ev,args) =
   let s = new_Type () in
-  Evd.evar_define ev s isevars, destSort s
+  Evd.evar_define ev s evd, destSort s
 
 
 (* We don't try to guess in which sort the type should be defined, since
@@ -872,33 +874,33 @@ let judge_of_new_Type () = Typeops.judge_of_type (new_univ ())
    constraint on its domain and codomain. If the input constraint is
    an evar instantiate it with the product of 2 new evars. *)
 
-let split_tycon loc env isevars tycon = 
+let split_tycon loc env evd tycon = 
   let rec real_split c = 
-    let sigma = evars_of isevars in
+    let sigma = evars_of evd in
     let t = whd_betadeltaiota env sigma c in
       match kind_of_term t with
-	| Prod (na,dom,rng) -> isevars, (na, dom, rng)
-	| Evar ev when not (Evd.is_defined_evar isevars ev) ->
-	    let (isevars',prod) = define_evar_as_arrow isevars ev in
+	| Prod (na,dom,rng) -> evd, (na, dom, rng)
+	| Evar ev when not (Evd.is_defined_evar evd ev) ->
+	    let (evd',prod) = define_evar_as_arrow evd ev in
 	    let (_,dom,rng) = destProd prod in
-	      isevars',(Anonymous, dom, rng)
+	      evd',(Anonymous, dom, rng)
 	| _ -> error_not_product_loc loc env sigma c
   in
     match tycon with
-      | None -> isevars,(Anonymous,None,None)
+      | None -> evd,(Anonymous,None,None)
       | Some (abs, c) ->
 	  (match abs with
 	       None -> 
-		 let isevars', (n, dom, rng) = real_split c in
-		   isevars', (n, mk_tycon dom, mk_tycon rng)
+		 let evd', (n, dom, rng) = real_split c in
+		   evd', (n, mk_tycon dom, mk_tycon rng)
 	     | Some (init, cur) ->
 		 if cur = 0 then 
-		   let isevars', (x, dom, rng) = real_split c in
-		     isevars, (Anonymous, 
+		   let evd', (x, dom, rng) = real_split c in
+		     evd, (Anonymous, 
 			       Some (Some (init, 0), dom), 
 			       Some (Some (init, 0), rng))
 		 else
-		   isevars, (Anonymous, None, Some (Some (init, pred cur), c)))
+		   evd, (Anonymous, None, Some (Some (init, pred cur), c)))
 
 let valcon_of_tycon x = 
   match x with
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 7c06b2aef..cf9694b34 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -69,7 +69,7 @@ let define evd ev body =
       evar_body = Evar_defined body } in
   match oldinfo.evar_body with
     | Evar_empty -> Evarmap.add ev newinfo evd
-    | _ -> anomaly "Evd.define: cannot define an isevar twice"
+    | _ -> anomaly "Evd.define: cannot define an evar twice"
     
 let is_evar sigma ev = mem sigma ev
 
@@ -408,8 +408,8 @@ let evar_source ev d =
   with Not_found -> (dummy_loc, InternalHole)
 
 (* define the existential of section path sp as the constr body *)
-let evar_define sp body isevars =
-  {isevars with evars = define isevars.evars sp body}
+let evar_define sp body evd =
+  {evd with evars = define evd.evars sp body}
 
 let evar_declare hyps evn ty ?(src=(dummy_loc,InternalHole)) evd =
   { evd with
@@ -420,24 +420,24 @@ let evar_declare hyps evn ty ?(src=(dummy_loc,InternalHole)) evd =
        evar_extra=None};
     history = (evn,src)::evd.history }
 
-let is_defined_evar isevars (n,_) = is_defined isevars.evars n
+let is_defined_evar evd (n,_) = is_defined evd.evars n
 
 (* Does k corresponds to an (un)defined existential ? *)
-let is_undefined_evar isevars c = match kind_of_term c with
-  | Evar ev -> not (is_defined_evar isevars ev)
+let is_undefined_evar evd c = match kind_of_term c with
+  | Evar ev -> not (is_defined_evar evd ev)
   | _ -> false
 
-let undefined_evars isevars = 
-  let evd = 
+let undefined_evars evd = 
+  let evars = 
     fold (fun ev evi sigma -> if evi.evar_body = Evar_empty then 
 	    add sigma ev evi else sigma) 
-      isevars.evars empty
+      evd.evars empty
   in 
-    { isevars with evars = evd }
+    { evd with evars = evars }
 
 (* extracts conversion problems that satisfy predicate p *)
 (* Note: conv_pbs not satisying p are stored back in reverse order *)
-let get_conv_pbs isevars p =
+let get_conv_pbs evd p =
   let (pbs,pbs1) = 
     List.fold_left
       (fun (pbs,pbs1) pb ->
@@ -446,13 +446,13 @@ let get_conv_pbs isevars p =
          else 
 	   (pbs,pb::pbs1))
       ([],[])
-      isevars.conv_pbs
+      evd.conv_pbs
   in
-  {isevars with conv_pbs = pbs1},
+  {evd with conv_pbs = pbs1},
   pbs
 
-let evar_merge isevars evars =
-  { isevars with evars = merge isevars.evars evars }
+let evar_merge evd evars =
+  { evd with evars = merge evd.evars evars }
 
 (**********************************************************)
 (* Sort variables *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 5f307cd69..9ecd7e251 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -171,24 +171,24 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
   let allow_anonymous_refs = ref false
 
-  let evd_comb0 f isevars =
-    let (evd',x) = f !isevars in
-      isevars := evd';
+  let evd_comb0 f evdref =
+    let (evd',x) = f !evdref in
+      evdref := evd';
       x
 
-  let evd_comb1 f isevars x =
-    let (evd',y) = f !isevars x in
-      isevars := evd';
+  let evd_comb1 f evdref x =
+    let (evd',y) = f !evdref x in
+      evdref := evd';
       y
 
-  let evd_comb2 f isevars x y =
-    let (evd',z) = f !isevars x y in
-      isevars := evd';
+  let evd_comb2 f evdref x y =
+    let (evd',z) = f !evdref x y in
+      evdref := evd';
       z
 
-  let evd_comb3 f isevars x y z =
-    let (evd',t) = f !isevars x y z in
-      isevars := evd';
+  let evd_comb3 f evdref x y z =
+    let (evd',t) = f !evdref x y z in
+      evdref := evd';
       t
 	
   let mt_evd = Evd.empty
@@ -198,27 +198,27 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   (* Faudra préférer une unification entre les types de toutes les clauses *)
   (* et autoriser des ? à rester dans le résultat de l'unification *)
   
-  let evar_type_fixpoint loc env isevars lna lar vdefj =
+  let evar_type_fixpoint loc env evdref lna lar vdefj =
     let lt = Array.length vdefj in 
       if Array.length lar = lt then 
 	for i = 0 to lt-1 do 
-          if not (e_cumul env isevars (vdefj.(i)).uj_type
+          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 !isevars)
+            error_ill_typed_rec_body_loc loc env (evars_of !evdref)
               i lna vdefj lar
 	done
 
-  let check_branches_message loc env isevars c (explft,lft) = 
+  let check_branches_message loc env evdref 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
+      if not (e_cumul env evdref lft.(i) explft.(i)) then 
+	let sigma = evars_of !evdref in
 	  error_ill_formed_branch_loc loc env sigma c i lft.(i) explft.(i)
     done
 
   (* coerce to tycon if any *)
-  let inh_conv_coerce_to_tycon loc env isevars j = function
+  let inh_conv_coerce_to_tycon loc env evdref j = function
     | None -> j
-    | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) isevars j t
+    | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) evdref j t
 
   let push_rels vars env = List.fold_right push_rel vars env
 
@@ -272,7 +272,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   (*************************************************************************)
   (* Main pretyping function                                               *)
 
-  let pretype_ref isevars env ref = 
+  let pretype_ref evdref env ref = 
     let c = constr_of_global ref in
       make_judge c (Retyping.get_type_of env Evd.empty c)
 
@@ -282,30 +282,30 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 
   exception Found of fixpoint
 
-  (* [pretype tycon env isevars lvar lmeta cstr] attempts to type [cstr] *)
-  (* in environment [env], with existential variables [(evars_of isevars)] and *)
+  (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *)
+  (* in environment [env], with existential variables [evdref] and *)
   (* the type constraint tycon *)
-  let rec pretype (tycon : type_constraint) env isevars lvar = function
+  let rec pretype (tycon : type_constraint) env evdref lvar = function
     | RRef (loc,ref) ->
-	inh_conv_coerce_to_tycon loc env isevars
-	  (pretype_ref isevars env ref)
+	inh_conv_coerce_to_tycon loc env evdref
+	  (pretype_ref evdref env ref)
 	  tycon
 
     | RVar (loc, id) ->
-	inh_conv_coerce_to_tycon loc env isevars
+	inh_conv_coerce_to_tycon loc env evdref
 	  (pretype_id loc env lvar id)
 	  tycon
 
-    | REvar (loc, ev, instopt) ->
+    | 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_context (Evd.find (evars_of !isevars) ev) in
+	let hyps = evar_context (Evd.find (evars_of !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 (ev, args) in
-	let j = (Retyping.get_judgment_of env (evars_of !isevars) c) in
-	  inh_conv_coerce_to_tycon loc env isevars j tycon
+	let c = mkEvar (evk, args) in
+	let j = (Retyping.get_judgment_of env (evars_of !evdref) c) in
+	  inh_conv_coerce_to_tycon loc env evdref j tycon
 
     | RPatVar (loc,(someta,n)) -> 
 	anomaly "Found a pattern variable in a rawterm to type"
@@ -315,26 +315,26 @@ module Pretyping_F (Coercion : Coercion.S) = struct
           match tycon with 
             | Some (None, ty) -> ty
             | None | Some _ ->
-		e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ()) in
-	  { uj_val = e_new_evar isevars env ~src:(loc,k) ty; uj_type = ty }
+		e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ()) in
+	  { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
 
     | RRec (loc,fixkind,names,bl,lar,vdef) ->
 	let rec type_bl env ctxt = function
             [] -> ctxt
           | (na,None,ty)::bl ->
-              let ty' = pretype_type empty_valcon env isevars lvar ty in
+              let ty' = pretype_type empty_valcon env evdref lvar ty in
               let dcl = (na,None,ty'.utj_val) in
 		type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl
           | (na,Some bd,ty)::bl ->
-              let ty' = pretype_type empty_valcon env isevars lvar ty in
-              let bd' = pretype (mk_tycon ty'.utj_val) env isevars lvar ty in
+              let ty' = pretype_type empty_valcon env evdref lvar ty in
+              let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar ty in
               let dcl = (na,Some bd'.uj_val,ty'.utj_val) in
 		type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl in
 	let ctxtv = Array.map (type_bl env empty_rel_context) bl in
 	let larj =
           array_map2
             (fun e ar ->
-               pretype_type empty_valcon (push_rel_context e env) isevars lvar ar)
+               pretype_type empty_valcon (push_rel_context e env) evdref lvar ar)
             ctxtv lar in
 	let lara = Array.map (fun a -> a.utj_val) larj in
 	let ftys = array_map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in
@@ -351,11 +351,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		 decompose_prod_n_assum (rel_context_length ctxt)
                    (lift nbfix ftys.(i)) in
                let nenv = push_rel_context ctxt newenv in
-               let j = pretype (mk_tycon ty) nenv isevars lvar def in
+               let j = pretype (mk_tycon ty) nenv evdref lvar def in
 		 { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
 		   uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
             ctxtv vdef in
-	evar_type_fixpoint loc env isevars names ftys vdefj;
+	evar_type_fixpoint loc env evdref names ftys vdefj;
 	let fixj = match fixkind with
 	  | RFix (vn,i) ->
 	      (* First, let's find the guard indexes. *)
@@ -377,83 +377,83 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	      let cofix = (i,(names,ftys,Array.map j_val vdefj)) in
 	      (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);
 	      make_judge (mkCoFix cofix) ftys.(i) in
-	inh_conv_coerce_to_tycon loc env isevars fixj tycon
+	inh_conv_coerce_to_tycon loc env evdref fixj tycon
 
     | RSort (loc,s) ->
-	inh_conv_coerce_to_tycon loc env isevars (pretype_sort s) tycon
+	inh_conv_coerce_to_tycon loc env evdref (pretype_sort s) tycon
 
     | RApp (loc,f,args) -> 
-	let fj = pretype empty_tycon env isevars lvar f in
+	let fj = pretype empty_tycon env evdref lvar f in
  	let floc = loc_of_rawconstr f in
 	let rec apply_rec env n resj = function
 	  | [] -> resj
 	  | 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 resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in
+              let resty = whd_betadeltaiota env (evars_of !evdref) resj.uj_type in
       		match kind_of_term resty with
 		  | Prod (na,c1,c2) ->
-		      let hj = pretype (mk_tycon c1) env isevars lvar c in
+		      let hj = pretype (mk_tycon c1) env evdref lvar c in
 		      let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
 			apply_rec env (n+1) 
 			  { uj_val = value;
 			    uj_type = typ }
 			  rest
 		  | _ ->
-		      let hj = pretype empty_tycon env isevars lvar c in
+		      let hj = pretype empty_tycon env evdref lvar c in
 			error_cant_apply_not_functional_loc 
-			  (join_loc floc argloc) env (evars_of !isevars)
+			  (join_loc floc argloc) env (evars_of !evdref)
 	      		  resj [hj]
 	in
 	let resj = apply_rec env 1 fj args in
 	let resj =
-	  match evar_kind_of_term !isevars resj.uj_val with
+	  match evar_kind_of_term !evdref resj.uj_val with
 	  | App (f,args) ->
-              let f = whd_evar (Evd.evars_of !isevars) f in
+              let f = whd_evar (Evd.evars_of !evdref) f in
               begin match kind_of_term f with
               | Ind _ (* | Const _ *) ->
-	          let sigma = evars_of !isevars in
+	          let sigma = evars_of !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
               | _ -> resj end
 	  | _ -> resj in
-	inh_conv_coerce_to_tycon loc env isevars resj tycon
+	inh_conv_coerce_to_tycon loc env evdref resj tycon
 
     | RLambda(loc,name,c1,c2)      ->
-	let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon in
+	let (name',dom,rng) = evd_comb1 (split_tycon loc env) evdref tycon in
 	let dom_valcon = valcon_of_tycon dom in
-	let j = pretype_type dom_valcon env isevars lvar c1 in
+	let j = pretype_type dom_valcon env evdref lvar c1 in
 	let var = (name,None,j.utj_val) in
-	let j' = pretype rng (push_rel var env) isevars lvar c2 in 
+	let j' = pretype rng (push_rel var env) evdref lvar c2 in 
 	  judge_of_abstraction env (orelse_name name name') j j'
 
     | RProd(loc,name,c1,c2)        ->
-	let j = pretype_type empty_valcon env isevars lvar c1 in
+	let j = pretype_type empty_valcon env evdref lvar c1 in
 	let var = (name,j.utj_val) in
 	let env' = push_rel_assum var env in
-	let j' = pretype_type empty_valcon env' isevars lvar c2 in
+	let j' = pretype_type empty_valcon env' evdref lvar c2 in
 	let resj =
 	  try judge_of_product env name j j'
 	  with TypeError _ as e -> Stdpp.raise_with_loc loc e in
-	  inh_conv_coerce_to_tycon loc env isevars resj tycon
+	  inh_conv_coerce_to_tycon loc env evdref resj tycon
 	    
     | RLetIn(loc,name,c1,c2)      ->
-	let j = pretype empty_tycon env isevars lvar c1 in
+	let j = pretype empty_tycon env evdref lvar c1 in
 	let t = refresh_universes j.uj_type in
 	let var = (name,Some j.uj_val,t) in
         let tycon = lift_tycon 1 tycon in
-	let j' = pretype tycon (push_rel var env) isevars lvar c2 in
+	let j' = pretype tycon (push_rel var env) evdref lvar c2 in
 	  { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
 	    uj_type = subst1 j.uj_val j'.uj_type }
 
     | RLetTuple (loc,nal,(na,po),c,d) ->
-	let cj = pretype empty_tycon env isevars lvar c in
+	let cj = pretype empty_tycon env evdref lvar c in
 	let (IndType (indf,realargs)) = 
-	  try find_rectype env (evars_of !isevars) cj.uj_type
+	  try find_rectype env (evars_of !evdref) 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 (evars_of !evdref) cj 
 	in
 	let cstrs = get_constructors env indf in
 	  if Array.length cstrs <> 1 then
@@ -476,16 +476,16 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	      (match po with
 		 | 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_isevar !isevars pj.utj_val in
+		     let pj = pretype_type empty_valcon env_p evdref lvar p in
+		     let ccl = nf_isevar !evdref 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 fj = pretype (mk_tycon fty) env_f isevars lvar d in
+		     let fty = hnf_lam_applist env (evars_of !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 =
 		       let mis,_ = dest_ind_family indf in
@@ -495,14 +495,14 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 
 		 | None -> 
 		     let tycon = lift_tycon cs.cs_nargs tycon in
-		     let fj = pretype tycon env_f isevars lvar d in
+		     let fj = pretype tycon env_f evdref lvar d in
 		     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
-		     let ccl = nf_isevar !isevars fj.uj_type in
+		     let ccl = nf_isevar !evdref 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 (evars_of !evdref) 
 			   cj.uj_val in
 		     let ccl = refresh_universes ccl in
 		     let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
@@ -514,12 +514,12 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		       { uj_val = v; uj_type = ccl })
 
     | RIf (loc,c,(na,po),b1,b2) ->
-	let cj = pretype empty_tycon env isevars lvar c in
+	let cj = pretype empty_tycon env evdref lvar c in
 	let (IndType (indf,realargs)) = 
-	  try find_rectype env (evars_of !isevars) cj.uj_type
+	  try find_rectype env (evars_of !evdref) 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 (evars_of !evdref) cj in
 	let cstrs = get_constructors env indf in 
 	  if Array.length cstrs <> 2 then
             user_err_loc (loc,"",
@@ -537,11 +537,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  let pred,p = match po with
 	    | 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 pj = pretype_type empty_valcon env_p evdref lvar p in
+		let ccl = nf_evar (evars_of !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 isevars {uj_val = pred;
+		let jtyp = inh_conv_coerce_to_tycon loc env evdref {uj_val = pred;
 								     uj_type = typ} tycon 
 		in
 		  jtyp.uj_val, jtyp.uj_type
@@ -549,11 +549,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		let p = match tycon with
 		  | Some (None, ty) -> ty
 		  | None | Some _ ->
-                      e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ())
+                      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 !isevars) pred in
-	  let p = nf_evar (evars_of !isevars) p in
+	  let pred = nf_evar (evars_of !evdref) pred in
+	  let p = nf_evar (evars_of !evdref) 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
@@ -572,7 +572,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	    in
 	    let env_c = push_rels csgn env in 
 (* 	      msgnl (str "Pi is: " ++ Termops.print_constr_env env_c pi); *)
-	    let bj = pretype (mk_tycon pi) env_c isevars lvar b in
+	    let bj = pretype (mk_tycon pi) env_c evdref lvar b in
 	      it_mkLambda_or_LetIn bj.uj_val cs.cs_args in
 	  let b1 = f cstrs.(0) b1 in
 	  let b2 = f cstrs.(1) b2 in
@@ -585,74 +585,74 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 
     | RCases (loc,po,tml,eqns) ->
 	Cases.compile_cases loc
-	  ((fun vtyc env -> pretype vtyc env isevars lvar),isevars)
+	  ((fun vtyc env -> pretype vtyc env evdref lvar),evdref)
 	  tycon env (* loc *) (po,tml,eqns)
 
     | RCast (loc,c,k) ->
 	let cj =
 	  match k with
 	      CastCoerce ->
-		let cj = pretype empty_tycon env isevars lvar c in
-		  evd_comb1 (Coercion.inh_coerce_to_base loc env) isevars cj
+		let cj = pretype empty_tycon env evdref lvar c in
+		  evd_comb1 (Coercion.inh_coerce_to_base loc env) evdref cj
 	    | CastConv (k,t) ->
-		let tj = pretype_type empty_valcon env isevars lvar t in
-		let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in
+		let tj = pretype_type empty_valcon env evdref lvar t in
+		let cj = pretype (mk_tycon tj.utj_val) env evdref lvar c in
 		  (* User Casts are for helping pretyping, experimentally not to be kept*)
 		  (* ... except for Correctness *)
 		let v = mkCast (cj.uj_val, k, tj.utj_val) in
 		  { uj_val = v; uj_type = tj.utj_val }
 	in
-	  inh_conv_coerce_to_tycon loc env isevars cj tycon
+	  inh_conv_coerce_to_tycon loc env evdref cj tycon
 
     | 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 (evars_of !evdref) c) in
 	    j
-	      (*inh_conv_coerce_to_tycon loc env isevars j tycon*)
+	      (*inh_conv_coerce_to_tycon loc env evdref j tycon*)
 	else
 	  user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic"))
 
-  (* [pretype_type valcon env isevars lvar c] coerces [c] into a type *)
-  and pretype_type valcon env isevars lvar = function
+  (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
+  and pretype_type valcon env evdref lvar = function
     | RHole loc ->
 	(match valcon with
 	   | Some v ->
                let s =
-		 let sigma = evars_of !isevars in
+		 let sigma = evars_of !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
-                     | Evar v when is_Type (existential_type sigma v) -> 
-			 evd_comb1 (define_evar_as_sort) isevars v
+                     | Evar ev when is_Type (existential_type sigma ev) -> 
+			 evd_comb1 (define_evar_as_sort) evdref ev
                      | _ -> anomaly "Found a type constraint which is not a type"
                in
 		 { utj_val = v;
 		   utj_type = s }
 	   | None ->
 	       let s = new_Type_sort () in
-		 { utj_val = e_new_evar isevars env ~src:loc (mkSort s);
+		 { utj_val = e_new_evar evdref env ~src:loc (mkSort s);
 		   utj_type = s})
     | c ->
-	let j = pretype empty_tycon env isevars lvar c in
+	let j = pretype empty_tycon env evdref lvar c in
 	let loc = loc_of_rawconstr c in
-	let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) isevars j in
+	let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in
 	  match valcon with
 	    | None -> tj
 	    | Some v ->
-		if e_cumul env isevars v tj.utj_val then tj
+		if e_cumul env evdref 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 (evars_of !evdref) tj.utj_val v
 
-  let pretype_gen isevars env lvar kind c =
+  let pretype_gen evdref env lvar kind c =
     let c' = match kind with
       | OfType exptyp ->
 	  let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
-	    (pretype tycon env isevars lvar c).uj_val
+	    (pretype tycon env evdref lvar c).uj_val
       | IsType ->
-	  (pretype_type empty_valcon env isevars lvar c).utj_val in
-      nf_evar (evars_of !isevars) c'
+	  (pretype_type empty_valcon env evdref lvar c).utj_val in
+      nf_evar (evars_of !evdref) c'
 
   (* TODO: comment faire remonter l'information si le typage a resolu des
      variables du sigma original. il faudrait que la fonction de typage
@@ -660,30 +660,30 @@ module Pretyping_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 isevars,_ = consider_remaining_unif_problems env !isevars in
-    let j = j_nf_evar (evars_of isevars) j 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 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
+    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 j = j_nf_evar sigma j in
-      j
+    j
 
   (* Raw calls to the unsafe inference machine: boolean says if we must
      fail on unresolved evars; the unsafe_judgment list allows us to
      extend env with some bindings *)
 
   let ise_pretype_gen fail_evar sigma env lvar kind c =
-    let isevars = ref (Evd.create_evar_defs sigma) in
-    let c = pretype_gen isevars env lvar kind c in
-    let isevars,_ = consider_remaining_unif_problems env !isevars in
-    let c = nf_evar (evars_of isevars) c in
-      if fail_evar then check_evars env sigma isevars c;
-      isevars, c
+    let evdref = ref (Evd.create_evar_defs sigma) in
+    let c = pretype_gen evdref env lvar kind c in
+    let evd,_ = consider_remaining_unif_problems env !evdref in
+    let c = nf_evar (evars_of evd) c in
+    if fail_evar then check_evars env sigma evd c;
+    evd, c
 
   (** Entry points of the high-level type synthesis algorithm *)
 
@@ -699,12 +699,12 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   let understand_ltac sigma env lvar kind c =
     ise_pretype_gen false sigma env lvar kind c
       
-  let understand_tcc_evars isevars env kind c =
-    pretype_gen isevars env ([],[]) kind c
+  let understand_tcc_evars evdref env kind c =
+    pretype_gen evdref env ([],[]) kind c
 
   let understand_tcc sigma env ?expected_type:exptyp c =
-    let ev, t = ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c in
-      Evd.evars_of ev, t
+    let evd, t = ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c in
+    Evd.evars_of evd, t
 end
 
 module Default : S = Pretyping_F(Coercion.Default)