deuxieme vague de modifs: evar_defs fonctionnel

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

14 files changed, 531 insertions, 435 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 7be919320e..463788a226 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -63,7 +63,8 @@ let error_needs_inversion env x t =
 (* A) Typing old cases                                               *)
 (* This was previously in Indrec but creates existential holes       *)
 
-let mkExistential isevars env loc = new_isevar isevars env loc (new_Type ())
+let mkExistential isevars env loc =
+  e_new_isevar isevars env loc (new_Type ())
 
 let norec_branch_scheme env isevars cstr =
   let rec crec env = function
@@ -378,7 +379,7 @@ let push_history_pattern n current cont =
 *)
 type pattern_matching_problem =
     { env      : env;
-      isevars  : evar_defs;
+      isevars  : evar_defs ref;
       pred     : predicate_signature option;
       tomatch  : tomatch_stack;
       history  : pattern_continuation;
@@ -404,7 +405,7 @@ exception NotCoercible
 
 let inh_coerce_to_ind isevars env tmloc ty tyi =
   let (mib,mip) = Inductive.lookup_mind_specif env tyi in
-  let (ntys,_) = splay_prod env (evars_of isevars) mip.mind_nf_arity in
+  let (ntys,_) = splay_prod env (evars_of !isevars) mip.mind_nf_arity in
   let hole_source = match tmloc with 
     | Some loc -> fun i -> (loc, TomatchTypeParameter (tyi,i))
     | None -> fun _ -> (dummy_loc, InternalHole) in
@@ -412,12 +413,12 @@ let inh_coerce_to_ind isevars env tmloc ty tyi =
     List.fold_right
       (fun (na,ty) (env,evl,n) ->
 	 (push_rel (na,None,ty) env,
-	    (new_isevar isevars env (hole_source n) ty)::evl,n+1))
+	    (e_new_isevar isevars env (hole_source n) ty)::evl,n+1))
       ntys (env,[],1) in
   let expected_typ = applist (mkInd tyi,evarl) in
      (* devrait être indifférent d'exiger leq ou pas puisque pour 
         un inductif cela doit être égal *)
-  if the_conv_x_leq env isevars expected_typ ty then ty
+  if e_cumul env isevars expected_typ ty then ty
   else raise NotCoercible
 
 (* We do the unification for all the rows that contain
@@ -431,17 +432,17 @@ let unify_tomatch_with_patterns isevars env tmloc typ = function
       (let tyi = inductive_of_constructor c in
        try 
 	 let indtyp = inh_coerce_to_ind isevars env tmloc typ tyi in
-	 IsInd (typ,find_rectype env (evars_of isevars) typ)
+	 IsInd (typ,find_rectype env (evars_of !isevars) typ)
        with NotCoercible ->
 	 (* 2 cases : Not the right inductive or not an inductive at all *)
 	 try
-	   IsInd (typ,find_rectype env (evars_of isevars) typ)
+	   IsInd (typ,find_rectype env (evars_of !isevars) typ)
              (* will try to coerce later in check_and_adjust_constructor.. *)
 	 with Not_found ->
 	   NotInd (None,typ))
 	     (* error will be detected in check_all_variables *)
   | None -> 
-      try IsInd (typ,find_rectype env (evars_of isevars) typ)
+      try IsInd (typ,find_rectype env (evars_of !isevars) typ)
       with Not_found -> NotInd (None,typ)
 
 let coerce_row typing_fun isevars env cstropt tomatch =
@@ -929,7 +930,7 @@ let infer_predicate loc env isevars typs cstrs indf =
     (* Empiric normalization: p may depend in a irrelevant way on args of the*)
     (* cstr as in [c:{_:Alpha & Beta}] Cases c of (existS a b)=>(a,b) end *)
     let typs =
-      Array.map (local_strong (whd_betaevar empty_env (evars_of isevars))) typs
+      Array.map (local_strong (whd_betaevar empty_env (evars_of !isevars))) typs
     in
     let eqns = array_map2 prepare_unif_pb typs cstrs in
     (* First strategy: no dependencies at all *)
@@ -942,7 +943,7 @@ let infer_predicate loc env isevars typs cstrs indf =
       else
 	mkExistential isevars env (loc, CasesType)
     in
-    if array_for_all (fun (_,_,typ) -> the_conv_x_leq env isevars typ mtyp) eqns
+    if array_for_all (fun (_,_,typ) -> e_cumul env isevars 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
@@ -1127,7 +1128,7 @@ let find_predicate loc env isevars p typs cstrs current
   (IndType (indf,realargs)) tms =
   let (dep,pred) =
     match p with
-      | Some p -> abstract_predicate env (evars_of isevars) indf current tms p
+      | Some p -> abstract_predicate env (evars_of !isevars) indf current tms p
       | None -> infer_predicate loc env isevars typs cstrs indf in
   let typ = whd_beta (applist (pred, realargs)) in
   if dep then
@@ -1367,7 +1368,7 @@ and compile_generalization pb d rest =
 and compile_alias pb (deppat,nondeppat,d,t) rest =
   let history = simplify_history pb.history in
   let sign, newenv, mat =
-    insert_aliases pb.env (evars_of pb.isevars) (deppat,nondeppat,d,t) pb.mat in
+    insert_aliases pb.env (evars_of !(pb.isevars)) (deppat,nondeppat,d,t) pb.mat in
   let n = List.length sign in
 
   (* We had Gamma1; x:current; Gamma2 |- tomatch(x) and we rebind x to get *)
@@ -1585,7 +1586,7 @@ let prepare_predicate_from_tycon loc dep env isevars tomatchs c =
 	(n, l, env) in
   let n, allargs, env = List.fold_left cook (0, [], env) tomatchs in
   let allargs =
-    List.map (fun c -> lift n (nf_betadeltaiota env (evars_of isevars) c)) allargs in
+    List.map (fun c -> lift n (nf_betadeltaiota env (evars_of !isevars) c)) allargs in
   let rec build_skeleton env c =
     (* Don't put into normal form, it has effects on the synthesis of evars *)
  (* let c = whd_betadeltaiota env (evars_of isevars) c in *)
@@ -1699,21 +1700,21 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
   | (Some pred,x) ->
       let loc = loc_of_rawconstr pred in
       let dep, n, predj =
-	let isevars_copy = evars_of isevars in
+	let isevars_copy = evars_of !isevars in
         (* We first assume the predicate is non dependent *)
 	let ndep_arity = build_expected_arity env isevars false tomatchs in
         try
 	  false, nb_prod ndep_arity, typing_fun (mk_tycon ndep_arity) env pred
 	with PretypeError _ | TypeError _ |
 	    Stdpp.Exc_located (_,(PretypeError _ | TypeError _)) ->
-        evars_reset_evd isevars_copy isevars;
+        isevars := evars_reset_evd isevars_copy !isevars;
         (* We then assume the predicate is dependent *)
 	let dep_arity = build_expected_arity env isevars true tomatchs in
 	try
 	  true, nb_prod dep_arity, typing_fun (mk_tycon dep_arity) env pred
 	with PretypeError _ | TypeError _ |
 	  Stdpp.Exc_located (_,(PretypeError _ | TypeError _)) ->
-        evars_reset_evd isevars_copy isevars;
+        isevars := evars_reset_evd isevars_copy !isevars;
         (* Otherwise we attempt to type it without constraints, possibly *)
         (* failing with an error message; it may also be well-typed *)
 	(* but fails to satisfy arity constraints in case_dependent *)
@@ -1769,5 +1770,8 @@ let compile_cases loc (typing_fun,isevars) tycon env (predopt, tomatchl, eqns)=
   List.iter (check_unused_pattern env) matx;
   
   match tycon with
-    | Some p ->	Coercion.inh_conv_coerce_to loc env isevars j p
+    | Some p ->
+	let (evd',j) = Coercion.inh_conv_coerce_to loc env !isevars j p in
+        isevars := evd';
+        j
     | None -> j
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 54fdc2c098..de63ea5258 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -34,7 +34,7 @@ exception PatternMatchingError of env * pattern_matching_error
 (*s Used for old cases in pretyping *)
 
 val branch_scheme : 
-  env -> evar_defs -> bool -> inductive_family -> constr array
+  env -> evar_defs ref -> bool -> inductive_family -> constr array
 
 type ml_case_error =
   | MlCaseAbsurd
@@ -48,9 +48,12 @@ val pred_case_ml : (* raises [NotInferable] if not inferable *)
 (*s Compilation of pattern-matching. *)
 
 val compile_cases :
-  loc -> (type_constraint -> env -> rawconstr -> unsafe_judgment)
-  * evar_defs -> type_constraint -> env ->
-      (rawconstr option * rawconstr option ref) *
-      (rawconstr * (name * (loc * inductive * name list) option) ref) list *
-    (loc * identifier list * cases_pattern list * rawconstr) list ->
-    unsafe_judgment
+  loc ->
+  (type_constraint -> env -> rawconstr -> unsafe_judgment) *
+  evar_defs ref ->
+  type_constraint -> 
+  env ->
+  (rawconstr option * rawconstr option ref) *
+  (rawconstr * (name * (loc * inductive * name list) option) ref) list *
+  (loc * identifier list * cases_pattern list * rawconstr) list ->
+  unsafe_judgment
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 0df34169a5..7753ec7ed7 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -23,6 +23,7 @@ open Pattern
 open Tacexpr
 open Tacred
 open Pretype_errors
+open Evarutil
 
 (* *)
 let get_env   evc = Global.env_of_context evc.it
@@ -157,8 +158,9 @@ let connect_clenv gls clenv =
   { clenv with hook = wc }
 
 let clenv_wtactic f clenv =
-  let (sigma',mmap') = f (clenv.hook.sigma, clenv.env) in
-  {clenv with env = mmap' ; hook = {it=clenv.hook.it; sigma=sigma'}}
+  let (evd',mmap') =
+    f (create_evar_defs clenv.hook.sigma, clenv.env) in
+  {clenv with env = mmap' ; hook = {it=clenv.hook.it; sigma=evars_of evd'}}
 
 let mk_clenv_hnf_constr_type_of wc t =
   mk_clenv_from wc (t,w_hnf_constr wc (w_type_of wc t))
@@ -411,10 +413,9 @@ let clenv_independent clenv =
 let w_coerce wc c ctyp target =
   let j = make_judge c ctyp in
   let env = get_env wc in
-  let isevars = Evarutil.create_evar_defs wc.sigma in
-  let j' = Coercion.inh_conv_coerce_to dummy_loc env isevars j target in
-  (* faire quelque chose avec isevars ? *)
-  j'.uj_val
+  let isevars = create_evar_defs wc.sigma in
+  let (evd',j') = Coercion.inh_conv_coerce_to dummy_loc env isevars j target in
+  (evars_of evd',j'.uj_val)
 
 let clenv_constrain_dep_args hyps_only clause = function
   | [] -> clause 
@@ -427,7 +428,8 @@ let clenv_constrain_dep_args hyps_only clause = function
 	    try
 	      let k_typ = w_hnf_constr wc (clenv_instance_type clause k) in
 	      let c_typ = w_hnf_constr wc (w_type_of wc c) in
-	      let c' = w_coerce wc c c_typ k_typ in
+              (* faire quelque chose avec le sigma retourne ? *)
+	      let (_,c') = w_coerce wc c c_typ k_typ in
 	      clenv_unify true CONV (mkMeta k) c' clenv
 	    with _ ->
               clenv_unify true CONV (mkMeta k) c clenv)
@@ -485,7 +487,7 @@ let clenv_match_args s clause =
 	  with _ ->
 	  (* Try to coerce to the type of [k]; cannot merge with the
 	     previous case because Coercion does not handle Meta *)
-          let c' = w_coerce clause.hook c c_typ k_typ in
+          let (_,c') = w_coerce clause.hook c c_typ k_typ in
 	  try clenv_unify true CONV (mkMeta k) c' clause
 	  with PretypeError (env,CannotUnify (m,n)) ->
 	    Stdpp.raise_with_loc loc
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index ae5cafdf65..d3f36e7205 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -14,6 +14,7 @@ open Names
 open Term
 open Sign
 open Evd
+open Evarutil
 (*i*)
 
 (* [new_meta] is a generator of unique meta variables *)
@@ -56,7 +57,7 @@ val mk_clenv_type_of : wc -> constr -> wc clausenv
 val subst_clenv : (substitution -> 'a -> 'a) -> 
   substitution -> 'a clausenv -> 'a clausenv
 val clenv_wtactic :
-  (evar_map * meta_map -> evar_map * meta_map) -> wc clausenv -> wc clausenv
+  (evar_defs * meta_map -> evar_defs * meta_map) -> wc clausenv -> wc clausenv
 
 val connect_clenv : evar_info sigma -> 'a clausenv -> wc clausenv
 val clenv_assign : metavariable -> constr -> 'a clausenv -> 'a clausenv
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index ddbdf94b43..347bc7b8e5 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -77,16 +77,16 @@ let apply_coercion env p hj typ_cl =
 let inh_app_fun env isevars j = 
   let t = whd_betadeltaiota env (evars_of isevars) j.uj_type in
   match kind_of_term t with
-    | Prod (_,_,_) -> j
+    | Prod (_,_,_) -> (isevars,j)
     | Evar ev when not (is_defined_evar isevars ev) ->
-	let t = define_evar_as_arrow isevars ev in
-	{ uj_val = j.uj_val; uj_type = t }
+	let (isevars',t) = define_evar_as_arrow isevars ev in
+	(isevars',{ uj_val = j.uj_val; uj_type = t })
     | _ ->
        	(try
  	   let t,i1 = class_of1 env (evars_of isevars) j.uj_type in
       	   let p = lookup_path_to_fun_from i1 in
-           apply_coercion env p j t
-	 with Not_found -> j)
+           (isevars,apply_coercion env p j t)
+	 with Not_found -> (isevars,j))
 
 let inh_tosort_force env isevars j =
   try
@@ -99,13 +99,13 @@ let inh_tosort_force env isevars j =
 let inh_coerce_to_sort env isevars j =
   let typ = whd_betadeltaiota env (evars_of isevars) j.uj_type in
   match kind_of_term typ with
-    | Sort s -> { utj_val = j.uj_val; utj_type = s }
+    | Sort s -> (isevars,{ utj_val = j.uj_val; utj_type = s })
     | Evar ev when not (is_defined_evar isevars ev) ->
-	let s = define_evar_as_sort isevars ev in
-	{ utj_val = j.uj_val; utj_type = s }
+	let (isevars',s) = define_evar_as_sort isevars ev in
+	(isevars',{ utj_val = j.uj_val; utj_type = s })
     | _ ->
         let j1 = inh_tosort_force env isevars j in 
-	type_judgment env (j_nf_evar (evars_of isevars) j1) 
+	(isevars,type_judgment env (j_nf_evar (evars_of isevars) j1))
 
 let inh_coerce_to_fail env isevars c1 hj =
   let hj' =
@@ -116,33 +116,34 @@ let inh_coerce_to_fail env isevars c1 hj =
       apply_coercion env p hj t2
     with Not_found -> raise NoCoercion 
   in
-  if the_conv_x_leq env isevars hj'.uj_type c1 then 
-    hj'
-  else
-    raise NoCoercion
+  try (the_conv_x_leq env hj'.uj_type c1 isevars, hj')
+  with Reduction.NotConvertible -> raise NoCoercion
 
 let rec inh_conv_coerce_to_fail env isevars hj c1 =
   let {uj_val = v; uj_type = t} = hj in
-  if the_conv_x_leq env isevars t c1 then hj
-  else 
-    try 
+  try (the_conv_x_leq env t c1 isevars, hj)
+  with Reduction.NotConvertible ->
+    (try 
       inh_coerce_to_fail env isevars c1 hj
-    with NoCoercion ->  (* try ... with _ -> ... is BAD *)
+    with NoCoercion ->
       (match kind_of_term (whd_betadeltaiota env (evars_of isevars) t),
 	     kind_of_term (whd_betadeltaiota env (evars_of isevars) c1) with
 	 | Prod (_,t1,t2), Prod (name,u1,u2) -> 
              let v' = whd_betadeltaiota env (evars_of isevars) v in
-             if (match kind_of_term v' with
-                   | Lambda (_,v1,v2) ->
-                       the_conv_x env isevars v1 u1 (* leq v1 u1? *)
-                   | _  -> false)
+             let (evd',b) =
+               match kind_of_term v' with
+                 | Lambda (_,v1,v2) ->
+                     (try the_conv_x env v1 u1 isevars, true  (* leq v1 u1? *)
+                     with Reduction.NotConvertible -> (isevars, false))
+                 | _  -> (isevars,false) in
+             if b
              then 
 	       let (x,v1,v2) = destLambda v' in
                let env1 = push_rel (x,None,v1) env in
-               let h2 = inh_conv_coerce_to_fail env1 isevars 
+               let (evd'',h2) = inh_conv_coerce_to_fail env1 evd'
 			  {uj_val = v2; uj_type = t2 } u2 in
-               { uj_val = mkLambda (x, v1, h2.uj_val);
-                 uj_type = mkProd (x, v1, h2.uj_type) }
+               (evd'',{ uj_val = mkLambda (x, v1, h2.uj_val);
+                 uj_type = mkProd (x, v1, h2.uj_type) })
              else 
                (* Mismatch on t1 and u1 or not a lambda: we eta-expand *)
                (* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *)
@@ -151,57 +152,27 @@ let rec inh_conv_coerce_to_fail env isevars hj c1 =
 			     | Anonymous -> Name (id_of_string "x")
                              | _ -> name) in
                let env1 = push_rel (name,None,u1) env in
-               let h1 =
+               let (evd',h1) =
 		 inh_conv_coerce_to_fail env1 isevars
 		   {uj_val = mkRel 1; uj_type = (lift 1 u1) }
                    (lift 1 t1) in
-               let h2 = inh_conv_coerce_to_fail env1 isevars
+               let (evd'',h2) = inh_conv_coerce_to_fail env1 evd'
 			 { uj_val = mkApp (lift 1 v, [|h1.uj_val|]);
                            uj_type = subst1 h1.uj_val t2 }
                           u2
 	       in
-               { uj_val = mkLambda (name, u1, h2.uj_val);
-                 uj_type = mkProd (name, u1, h2.uj_type) }
-	 | _ -> raise NoCoercion)
+               (evd'',
+                { uj_val = mkLambda (name, u1, h2.uj_val);
+                  uj_type = mkProd (name, u1, h2.uj_type) })
+	 | _ -> 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 t =
-  let cj' = 
+  let (evd',cj') = 
     try 
       inh_conv_coerce_to_fail env isevars cj t
     with NoCoercion ->
       let sigma = evars_of isevars in
       error_actual_type_loc loc env sigma cj t
   in
-  { uj_val = cj'.uj_val; uj_type = t }
-
-(* [inh_apply_rel_list loc env isevars args f tycon] tries to type [(f
-   args)] of type [tycon] (if any) by inserting coercions in front of
-   each arg$_i$, if necessary *)
-
-let inh_apply_rel_list apploc env isevars argjl (funloc,funj) tycon =
-  let rec apply_rec env n resj = function
-    | [] -> resj
-    | (loc,hj)::restjl ->
-        let sigma = evars_of isevars in
-	let resj = inh_app_fun env isevars resj in
-        let ntyp = whd_betadeltaiota env sigma resj.uj_type in
-      	match kind_of_term ntyp with
-          | Prod (na,c1,c2) ->
-              let hj' =
-		try 
-		  inh_conv_coerce_to_fail env isevars hj c1
-		with NoCoercion ->
-                  error_cant_apply_bad_type_loc apploc env sigma
-		    (1,c1,hj.uj_type) resj (List.map snd restjl) in
-	      let newresj =
-      		{ uj_val = applist (j_val resj, [j_val hj']);
-		  uj_type = subst1 hj'.uj_val c2 } in
-	      apply_rec (push_rel (na,None,c1) env) (n+1) newresj restjl
-          | _ ->
-              error_cant_apply_not_functional_loc 
-		(join_loc funloc loc) env sigma resj
-                (List.map snd restjl)
-  in 
-  apply_rec env 1 funj argjl
-
+  (evd',{ uj_val = cj'.uj_val; uj_type = t })
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index cf24829c1d..85b4c7506e 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -25,19 +25,19 @@ open Rawterm
    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 -> unsafe_judgment
+  env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment
 
 (* [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it
    inserts a coercion into [j], if needed, in such a way it gets as
    type a sort; it fails if no coercion is applicable *)
 val inh_coerce_to_sort :
-  env -> evar_defs -> unsafe_judgment -> unsafe_type_judgment
+  env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_type_judgment
 
 (* [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type 
    [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
    [j.uj_type] are convertible; it fails if no coercion is applicable *)
 val inh_conv_coerce_to : loc -> 
-  env -> evar_defs -> unsafe_judgment -> constr -> unsafe_judgment
+  env -> evar_defs -> unsafe_judgment -> constr -> evar_defs * unsafe_judgment
 
 (* [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases
    pattern [pat] typed in [ind1] into a pattern typed in [ind2];
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3ca777647d..6454e0e84c 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -125,6 +125,44 @@ let check_conv_record (t1,l1) (t2,l2) =
 (* Precondition: one of the terms of the pb is an uninstanciated evar,
  * possibly applied to arguments. *)
 
+let rec ise_try isevars = function
+    [] -> assert false
+  | [f] -> f isevars
+  | f1::l ->
+      let (isevars',b) = f1 isevars in
+      if b then (isevars',b) else ise_try isevars l
+
+let ise_and isevars 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
+
+let ise_list2 isevars 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
+
+let ise_array2 isevars 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)
+  in 
+  let lv1 = Array.length v1 in
+  if lv1 = Array.length v2 then allrec isevars (pred lv1) 
+  else (isevars,false)
+
 let rec evar_conv_x env isevars pbty term1 term2 = 
   let sigma = evars_of isevars in
   let term1 = whd_castappevar sigma term1 in
@@ -136,11 +174,12 @@ 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  *)
-  (not (has_undefined_isevars isevars term1) &
-   not (has_undefined_isevars isevars term2) &
-   is_fconv pbty env (evars_of isevars) term1 term2) 
-  or
-  if ise_undefined isevars term1 then
+  if
+    (not (has_undefined_isevars isevars term1) &
+    not (has_undefined_isevars isevars term2) &
+    is_fconv pbty env (evars_of isevars) term1 term2) then
+      (isevars,true)
+  else if ise_undefined isevars term1 then
     solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term1,term2)
   else if ise_undefined isevars term2 then
     solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term2,term1)
@@ -150,7 +189,7 @@ let rec evar_conv_x env isevars pbty term1 term2 =
     if (head_is_embedded_evar isevars t1 & not(is_eliminator t2))
       or (head_is_embedded_evar isevars t2 & not(is_eliminator t1))
     then 
-      (add_conv_pb isevars (pbty,applist(t1,l1),applist(t2,l2)); true)
+      (add_conv_pb (pbty,applist(t1,l1),applist(t2,l2)) isevars, true)
     else 
       evar_eqappr_x env isevars pbty (t1,l1) (t2,l2)
 
@@ -158,67 +197,81 @@ and evar_eqappr_x env isevars 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) ->
-	let f1 () =
+	let f1 i =
 	  if List.length l1 > List.length l2 then 
             let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
-            solve_simple_eqn evar_conv_x env isevars 
-	      (pbty,ev2,applist(term1,deb1))
-            & list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2
+            ise_and i
+              [(fun i -> solve_simple_eqn evar_conv_x env i
+	        (pbty,ev2,applist(term1,deb1)));
+              (fun i -> ise_list2 i
+                  (fun i -> evar_conv_x env i CONV) rest1 l2)]
 	  else
 	    let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
-	    solve_simple_eqn evar_conv_x env isevars
-	      (pbty,ev1,applist(term2,deb2))
-            & list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2
-	and f2 () =
-          (sp1 = sp2)
-	  & (array_for_all2 (evar_conv_x env isevars CONV) al1 al2)  
-	  & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
+            ise_and i
+              [(fun i -> solve_simple_eqn evar_conv_x env i
+	          (pbty,ev1,applist(term2,deb2)));
+              (fun i -> ise_list2 i
+                  (fun i -> evar_conv_x env i CONV) l1 rest2)]
+	and f2 i =
+          if sp1 = sp2 then
+            ise_and i
+            [(fun i -> ise_array2 i
+                (fun i -> evar_conv_x env i CONV) al1 al2);
+             (fun i -> ise_list2 i
+                 (fun i -> evar_conv_x env i CONV) l1 l2)]
+          else (i,false)
 	in 
 	ise_try isevars [f1; f2]
 
     | Flexible ev1, MaybeFlexible flex2 ->
-	let f1 () =
-	  (List.length l1 <= List.length l2) &
-	  let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
-          (* First compare extra args for better failure message *)
-          list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2 &
-	  evar_conv_x env isevars pbty term1 (applist(term2,deb2))
-	and f4 () =
+	let f1 i =
+          if List.length l1 <= List.length l2 then
+	    let (deb2,rest2) =
+              list_chop (List.length l2-List.length l1) l2 in
+            ise_and i
+              (* First compare extra args for better failure message *)
+              [(fun i -> ise_list2 i
+                  (fun i -> evar_conv_x env i CONV) l1 rest2);
+               (fun i -> evar_conv_x env i pbty term1 (applist(term2,deb2)))]
+          else (i,false)
+	and f4 i =
 	  match eval_flexible_term env flex2 with
 	    | Some v2 ->
-		evar_eqappr_x env isevars pbty
-		  appr1 (evar_apprec env isevars l2 v2)
-	    | None -> false
+		evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2)
+	    | None -> (i,false)
 	in 
 	ise_try isevars [f1; f4]
 
     | MaybeFlexible flex1, Flexible ev2 ->
-	let f1 () =
-       	  (List.length l2 <= List.length l1) &
-       	  let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
-          (* First compare extra args for better failure message *)
-          list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2 &
-	  evar_conv_x env isevars pbty (applist(term1,deb1)) term2
-	and f4 () =
+	let f1 i =
+       	  if List.length l2 <= List.length l1 then
+            let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
+            ise_and i
+            (* 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 -> evar_conv_x env i pbty (applist(term1,deb1)) term2)]
+          else (i,false)
+	and f4 i =
 	  match eval_flexible_term env flex1 with
 	    | Some v1 ->
-		evar_eqappr_x env isevars pbty
-		  (evar_apprec env isevars l1 v1) appr2
-	    | None -> false
+		evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2
+	    | None -> (i,false)
 	in 
 	ise_try isevars [f1; f4]
 
     | MaybeFlexible flex1, MaybeFlexible flex2 ->
-	let f2 () =
-          (flex1 = flex2)
-	  & (List.length l1 = List.length l2)
-	  & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
-	and f3 () =
-	  (try conv_record env isevars 
+	let f2 i =
+          if flex1 = flex2 then
+            ise_list2 i (fun i -> evar_conv_x env i CONV) l1 l2
+          else (i,false)
+	and f3 i =
+	  (try conv_record env i
              (try check_conv_record appr1 appr2
 	      with Not_found -> check_conv_record appr2 appr1)
-           with _ -> false)
-	and f4 () =
+(* TODO: remove this _ !!! *)
+           with _ -> (i,false))
+	and f4 i =
           (* heuristic: unfold second argument first, exception made
              if the first argument is a beta-redex (expand a constant
              only if necessary) *)
@@ -228,57 +281,55 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
               | _ -> eval_flexible_term env flex2 in
 	  match val2 with
 	    | Some v2 ->
-		evar_eqappr_x env isevars pbty
-		  appr1 (evar_apprec env isevars l2 v2)
+		evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2)
 	    | None ->
 		match eval_flexible_term env flex1 with
 		  | Some v1 ->
-		      evar_eqappr_x env isevars pbty
-			(evar_apprec env isevars l1 v1) appr2
-		  | None -> false
+		      evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2
+		  | None -> (i,false)
 	in 
 	ise_try isevars [f2; f3; f4]
 
     | Flexible ev1, Rigid _ ->
-       	(List.length l1 <= List.length l2) &
-       	let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
-        (* First compare extra args for better failure message *)
-        list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2 &
-	solve_simple_eqn evar_conv_x env isevars
-	  (pbty,ev1,applist(term2,deb2))
-
+       	if (List.length l1 <= List.length l2) then
+       	  let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
+          ise_and isevars
+            (* First compare extra args for better failure message *)
+            [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) l1 rest2);
+             (fun i -> solve_simple_eqn evar_conv_x env i
+                 (pbty,ev1,applist(term2,deb2)))]
+        else (isevars,false)
     | Rigid _, Flexible ev2 ->
-       	(List.length l2 <= List.length l1) &
-       	let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
-        (* First compare extra args for better failure message *)
-        list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2 &
-	solve_simple_eqn evar_conv_x env isevars
-	  (pbty,ev2,applist(term1,deb1))
-        
+        if List.length l2 <= List.length l1 then
+       	  let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
+          ise_and isevars
+            (* 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 -> solve_simple_eqn evar_conv_x env i
+	         (pbty,ev2,applist(term1,deb1)))]
+        else (isevars,false)
 
     | MaybeFlexible flex1, Rigid _ ->
-	let f3 () =
-	  (try conv_record env isevars (check_conv_record appr1 appr2)
-           with _ -> false)
-	and f4 () =
+	let f3 i =
+	  (try conv_record env i (check_conv_record appr1 appr2)
+           with _ -> (i,false))
+	and f4 i =
 	  match eval_flexible_term env flex1 with
 	    | Some v1 ->
- 		evar_eqappr_x env isevars pbty
-		  (evar_apprec env isevars l1 v1) appr2
-	    | None -> false
+ 		evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2
+	    | None -> (i,false)
 	in 
 	ise_try isevars [f3; f4]
 	     
     | Rigid _ , MaybeFlexible flex2 -> 
-	let f3 () = 
-	  (try (conv_record env isevars (check_conv_record appr2 appr1))
-           with _ -> false)
-	and f4 () =
+	let f3 i = 
+	  (try (conv_record env i (check_conv_record appr2 appr1))
+           with _ -> (i,false))
+	and f4 i =
 	  match eval_flexible_term env flex2 with
 	    | Some v2 ->
- 		evar_eqappr_x env isevars pbty
-		  appr1 (evar_apprec env isevars l2 v2)
-	    | None -> false
+ 		evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2)
+	    | None -> (i,false)
 	in 
 	ise_try isevars [f3; f4]
 
@@ -288,27 +339,30 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 
 	| _, Cast (c2,_) -> evar_eqappr_x env isevars pbty appr1 (c2,l2)
 
-	| Sort s1, Sort s2 when l1=[] & l2=[] -> base_sort_cmp pbty s1 s2
+	| Sort s1, Sort s2 when l1=[] & l2=[] ->
+            (isevars,base_sort_cmp pbty s1 s2)
 
 	| Lambda (na,c1,c'1), Lambda (_,c2,c'2) when l1=[] & l2=[] -> 
-	    evar_conv_x env isevars CONV c1 c2
-	    & 
-	    (let c = nf_evar (evars_of isevars) c1 in
-             evar_conv_x (push_rel (na,None,c) env) isevars CONV c'1 c'2)
+            ise_and isevars
+              [(fun i -> evar_conv_x env i CONV c1 c2);
+               (fun i ->
+                 let c = nf_evar (evars_of i) c1 in
+                 evar_conv_x (push_rel (na,None,c) env) i CONV c'1 c'2)]
 
 	| LetIn (na,b1,t1,c'1), LetIn (_,b2,_,c'2) ->
-	    let f1 () =
-	      evar_conv_x env isevars CONV b1 b2
-	      & 
-              (let b = nf_evar (evars_of isevars) b1 in
-	       let t = nf_evar (evars_of isevars) t1 in
-               evar_conv_x (push_rel (na,Some b,t) env) isevars pbty c'1 c'2)
-	      & (List.length l1 = List.length l2)
-	      & (List.for_all2 (evar_conv_x env isevars CONV) l1 l2)
-	    and f2 () =
-              let appr1 = evar_apprec env isevars l1 (subst1 b1 c'1)
-              and appr2 = evar_apprec env isevars l2 (subst1 b2 c'2)
-	      in evar_eqappr_x env isevars pbty appr1 appr2
+	    let f1 i =
+              ise_and i
+                [(fun i -> evar_conv_x env i CONV b1 b2);
+                 (fun i ->
+                   let b = nf_evar (evars_of i) b1 in
+	           let t = nf_evar (evars_of i) t1 in
+                   evar_conv_x (push_rel (na,Some b,t) env) i pbty c'1 c'2);
+                 (fun i -> ise_list2 i
+                     (fun i -> evar_conv_x env i CONV) l1 l2)]
+	    and f2 i =
+              let appr1 = evar_apprec env i l1 (subst1 b1 c'1)
+              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]
 
@@ -321,71 +375,102 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
             in evar_eqappr_x env isevars pbty appr1 appr2
 
 	| Prod (n,c1,c'1), Prod (_,c2,c'2) when l1=[] & l2=[] -> 
-            evar_conv_x env isevars CONV c1 c2
-            & 
-	    (let c = nf_evar (evars_of isevars) c1 in
-	     evar_conv_x (push_rel (n,None,c) env) isevars pbty c'1 c'2)
+            ise_and isevars
+              [(fun i -> evar_conv_x env i CONV c1 c2);
+               (fun i ->
+ 	         let c = nf_evar (evars_of i) c1 in
+	         evar_conv_x (push_rel (n,None,c) env) i pbty c'1 c'2)]
 
 	| Ind sp1, Ind sp2 ->
-	    sp1=sp2
-            & list_for_all2eq (evar_conv_x env isevars CONV) l1 l2
-             
+	    if sp1=sp2 then
+              ise_list2 isevars (fun i -> evar_conv_x env i CONV) l1 l2
+            else (isevars, false)
+
 	| Construct sp1, Construct sp2 ->
-	    sp1=sp2
-            & list_for_all2eq (evar_conv_x env isevars CONV) l1 l2
+	    if sp1=sp2 then
+              ise_list2 isevars (fun i -> evar_conv_x env i CONV) l1 l2
+            else (isevars, false)
 
 	| Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
-	    evar_conv_x env isevars CONV p1 p2
-	    & evar_conv_x env isevars CONV c1 c2
-	    & (array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2)
-	    & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
+            ise_and isevars
+              [(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
+                   (fun i -> evar_conv_x env i CONV) cl1 cl2);
+               (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) l1 l2)]
 
 	| Fix (li1,(_,tys1,bds1 as recdef1)), Fix (li2,(_,tys2,bds2)) ->
-	    li1=li2
-	    & (array_for_all2 (evar_conv_x env isevars CONV) tys1 tys2)
-	    & (array_for_all2
-		 (evar_conv_x (push_rec_types recdef1 env) isevars CONV)
-		 bds1 bds2)
-	    & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
-	     
+            if li1=li2 then
+              ise_and isevars
+                [(fun i -> ise_array2 i
+                    (fun i -> evar_conv_x env i CONV) tys1 tys2);
+                 (fun i -> ise_array2 i
+		     (fun i -> evar_conv_x (push_rec_types recdef1 env) i CONV)
+		     bds1 bds2);
+	         (fun i -> ise_list2 i
+                     (fun i -> evar_conv_x env i CONV) l1 l2)]
+	    else (isevars,false)
 	| CoFix (i1,(_,tys1,bds1 as recdef1)), CoFix (i2,(_,tys2,bds2)) ->
-	    i1=i2 
-	    & (array_for_all2 (evar_conv_x env isevars CONV) tys1 tys2)
-	    & (array_for_all2
-		 (evar_conv_x (push_rec_types recdef1 env) isevars CONV)
-		 bds1 bds2)
-	    & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
-
-	| (Meta _ | Lambda _), _ -> false
-	| _, (Meta _ | Lambda _) -> false
-
-	| (Ind _ | Construct _ | Sort _ | Prod _), _ -> false
-	| _, (Ind _ | Construct _ | Sort _ | Prod _) -> false
+            if i1=i2  then
+              ise_and isevars
+                [(fun i -> ise_array2 i
+                    (fun i -> evar_conv_x env i CONV) tys1 tys2);
+                 (fun i -> ise_array2 i
+		     (fun i -> evar_conv_x (push_rec_types recdef1 env) i CONV)
+		     bds1 bds2);
+                 (fun i -> ise_list2 i
+                     (fun i -> evar_conv_x env i CONV) l1 l2)]
+            else (isevars,false)
+
+	| (Meta _ | Lambda _), _ -> (isevars,false)
+	| _, (Meta _ | Lambda _) -> (isevars,false)
+
+	| (Ind _ | Construct _ | Sort _ | Prod _), _ -> (isevars,false)
+	| _, (Ind _ | Construct _ | Sort _ | Prod _) -> (isevars,false)
 
 	| (App _ | Case _ | Fix _ | CoFix _), 
-	  (App _ | Case _ | Fix _ | CoFix _) -> false
+	  (App _ | Case _ | Fix _ | CoFix _) -> (isevars,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 ks =
+  let (isevars',ks) =
     List.fold_left
-      (fun ks b ->
+      (fun (i,ks) b ->
 	 let dloc = (dummy_loc,Rawterm.InternalHole) in
-	 (new_isevar isevars env dloc (substl ks b)) :: ks)
-      [] bs
+         let (i',ev) = new_isevar i env dloc (substl ks b) in
+	 (i', ev :: ks))
+      (isevars,[]) bs
   in
-  (list_for_all2eq 
-     (fun u1 u -> evar_conv_x env isevars CONV u1 (substl ks u))
-     us2 us)
-  &
-  (list_for_all2eq 
-     (fun x1 x -> evar_conv_x env isevars CONV x1 (substl ks x))
-     params1 params)
-  & (list_for_all2eq (evar_conv_x env isevars CONV) ts ts1)
-  & (evar_conv_x env isevars CONV c1 (applist (c,(List.rev ks))))
+  ise_and isevars'
+    [(fun i ->
+      ise_list2 i
+        (fun i u1 u -> evar_conv_x env i CONV u1 (substl ks u))
+        us2 us);
+     (fun i ->
+       ise_list2 i
+         (fun i x1 x -> evar_conv_x env i CONV x1 (substl ks x))
+         params1 params);
+     (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 the_conv_x     env isevars t1 t2 = evar_conv_x env isevars CONV  t1 t2
-let the_conv_x_leq env isevars t1 t2 = evar_conv_x env isevars CUMUL t1 t2
+let the_conv_x     env t1 t2 isevars =
+  match evar_conv_x env isevars 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
+      (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
+    | _ -> false
+
+let e_cumul env isevars t1 t2 =
+  match evar_conv_x env !isevars CUMUL t1 t2 with
+      (evd',true) -> isevars := evd'; true
+    | _ -> false
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index c8b234ee29..5deccaa8b1 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -16,13 +16,20 @@ open Reductionops
 open Evarutil
 (*i*)
 
-val the_conv_x : env -> evar_defs -> constr -> constr -> bool
+(* returns exception Reduction.NotConvertible if not unifiable *)
+val the_conv_x     : env -> constr -> constr -> evar_defs -> evar_defs
+val the_conv_x_leq : env -> constr -> constr -> evar_defs -> evar_defs
 
-val the_conv_x_leq : env -> evar_defs -> constr -> constr -> bool
+(* The same function resolving evars by side-effect and 
+   catching the exception *)
+val e_conv  : env -> evar_defs ref -> constr -> constr -> bool
+val e_cumul : env -> evar_defs ref -> constr -> constr -> bool
 
 (*i For debugging *)
-val evar_conv_x : env -> evar_defs -> conv_pb -> constr -> constr -> bool
+val evar_conv_x :
+  env -> evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool
 val evar_eqappr_x : 
   env -> evar_defs ->
-    conv_pb -> constr * constr list -> constr * constr list -> bool
+    conv_pb -> constr * constr list -> constr * constr list ->
+      evar_defs * bool
 (*i*)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index f5b8c6288d..aa079e7ceb 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -218,32 +218,18 @@ let do_restrict_hyps sigma ev args =
 
 type evar_constraint = conv_pb * constr * constr
 type evar_defs =
-    { mutable evars : Evd.evar_map;
-      mutable conv_pbs : evar_constraint list;
-      mutable history : (existential_key * (loc * Rawterm.hole_kind)) list }
+    { evars : Evd.evar_map;
+      conv_pbs : evar_constraint list;
+      history : (existential_key * (loc * Rawterm.hole_kind)) list }
 
 let create_evar_defs evd = { evars=evd; conv_pbs=[]; history=[] }
 let evars_of d = d.evars
-let evars_reset_evd evd d = d.evars <- evd
-let add_conv_pb d pb = d.conv_pbs <- pb::d.conv_pbs
+let evars_reset_evd evd d = {d with evars = evd}
+let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs}
 let evar_source ev d =
   try List.assoc ev d.history
   with Failure _ -> (dummy_loc, Rawterm.InternalHole)
 
-(* ise_try [f1;...;fn] tries fi() for i=1..n, restoring the evar constraints
- * when fi returns false or an exception. Returns true if one of the fi
- * returns true, and false if every fi return false (in the latter case,
- * the evar constraints are restored).
- *)
-let ise_try isevars l =
-  let u = isevars.evars in
-  let rec test = function
-      [] -> isevars.evars <- u; false
-    | f::l ->
- 	  (try f() with reraise -> isevars.evars <- u; raise reraise)
-       or (isevars.evars <- u; test l)
-  in test l
-
 (* say if the section path sp corresponds to an existential *)
 let ise_in_dom isevars sp = Evd.in_dom isevars.evars sp
 
@@ -253,7 +239,7 @@ let ise_map isevars sp = Evd.map isevars.evars sp
 (* define the existential of section path sp as the constr body *)
 let ise_define isevars sp body =
   let body = refresh_universes body in (* needed only if an inferred type *)
-  isevars.evars <- Evd.define isevars.evars sp body
+  {isevars with evars = Evd.define isevars.evars sp body}
 
 let is_defined_evar isevars (n,_) = Evd.is_defined isevars.evars n
 
@@ -283,6 +269,7 @@ let non_instantiated sigma =
  *)
 
 let real_clean env isevars ev args rhs =
+  let evd = ref isevars in
   let subst = List.map (fun (x,y) -> (y,mkVar x)) (filter_unique args) in
   let rec subs k t =
     match kind_of_term t with
@@ -296,9 +283,11 @@ let real_clean env isevars ev args rhs =
 	      subs k (existential_value isevars.evars (ev,args'))
 	    else begin
 	      let (sigma,rc) = do_restrict_hyps isevars.evars ev args' in
-	      isevars.evars <- sigma;
-              isevars.history <- 
-                (fst (destEvar rc),evar_source ev isevars)::isevars.history;
+              evd :=
+	      {!evd with
+               evars = sigma;
+               history = 
+                (fst (destEvar rc),evar_source ev isevars):: !evd.history};
 	      rc
 	    end
 	  else
@@ -309,7 +298,7 @@ let real_clean env isevars ev args rhs =
   let body = subs 0 rhs in
   if not (closed0 body)
   then error_not_clean env isevars.evars ev body (evar_source ev isevars);
-  body
+  (!evd,body)
 
 let make_evar_instance_with_rel env =
   let n = rel_context_length (rel_context env) in
@@ -354,10 +343,17 @@ let new_isevar isevars env src typ =
   let typ' = substl subst typ in
   let instance = make_evar_instance_with_rel env in
   let (sigma',evar) = new_isevar_sign env' isevars.evars typ' instance in
-  isevars.evars <- sigma';
-  isevars.history <- (fst (destEvar evar),src)::isevars.history;
+  {isevars with
+   evars = sigma';
+   history = (fst (destEvar evar),src)::isevars.history},
   evar
 
+(* The same using side-effect *)
+let e_new_isevar isevars env loc ty =
+  let (evd',ev) = new_isevar !isevars env loc ty in
+  isevars := evd';
+  ev
+
 (* [evar_define] solves the problem lhs = rhs when lhs is an uninstantiated
  * evar, i.e. tries to find the body ?sp for lhs=mkEvar (sp,args)
  * ?sp [ sp.hyps \ args ]  unifies to rhs
@@ -380,12 +376,12 @@ let evar_define env isevars (ev,argsv) rhs =
   if occur_evar ev rhs
   then error_occur_check env (evars_of isevars) ev rhs;
   let args = Array.to_list argsv in 
-  let evd = ise_map isevars ev in
+  let evi = ise_map isevars ev in
   (* the bindings to invert *)
-  let worklist = make_subst (evar_env evd) args in
-  let body = real_clean env isevars ev worklist rhs in
-  ise_define isevars ev body;
-  [ev]
+  let worklist = make_subst (evar_env evi) args in
+  let (isevars',body) = real_clean env isevars ev worklist rhs in
+  let isevars'' = ise_define isevars' ev body in
+  isevars'',[ev]
 
 (*-------------------*)
 (* Auxiliary functions for the conversion algorithms modulo evars
@@ -466,7 +462,7 @@ let get_changed_pb isevars lev =
       ([],[])
       isevars.conv_pbs
   in
-  isevars.conv_pbs <- pbs1;
+  {isevars with conv_pbs = pbs1},
   pbs
 
 (* Solve pbs (?i x1..xn) = (?i y1..yn) which arises often in fixpoint
@@ -475,26 +471,28 @@ let get_changed_pb isevars lev =
  * depend on these args). *)
 
 let solve_refl conv_algo env isevars ev argsv1 argsv2 =
-  if argsv1 = argsv2 then [] else
+  if argsv1 = argsv2 then (isevars,[]) else
   let evd = Evd.map isevars.evars ev in
   let hyps = evd.evar_hyps in
-  let (_,rsign) = 
+  let (isevars',_,rsign) = 
     array_fold_left2
-      (fun (sgn,rsgn) a1 a2 ->
-	 if conv_algo env isevars CONV a1 a2 then 
-	   (List.tl sgn, add_named_decl (List.hd sgn) rsgn)
+      (fun (isevars,sgn,rsgn) a1 a2 ->
+        let (isevars',b) = conv_algo env isevars CONV a1 a2 in
+	 if b then 
+	   (isevars',List.tl sgn, add_named_decl (List.hd sgn) rsgn)
 	 else 
-	   (List.tl  sgn, rsgn))
-      (hyps,[]) argsv1 argsv2 
+	   (isevars,List.tl  sgn, rsgn))
+      (isevars,hyps,[]) argsv1 argsv2 
   in
   let nsign = List.rev rsign in
   let nargs = (Array.of_list (List.map mkVar (ids_of_named_context nsign))) in
   let newev = new_evar () in
   let info = { evar_concl = evd.evar_concl; evar_hyps = nsign;
 	       evar_body = Evar_empty } in
-  isevars.evars <-
+  {isevars with
+   evars =
     Evd.define (Evd.add isevars.evars newev info) ev (mkEvar (newev,nargs));
-  isevars.history <- (newev,evar_source ev isevars)::isevars.history;
+   history = (newev,evar_source ev isevars)::isevars.history},
   [ev]
 
 
@@ -506,7 +504,7 @@ let solve_refl conv_algo env isevars ev argsv1 argsv2 =
 (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *)
 let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) =
   let t2 = nf_evar isevars.evars t2 in
-  let lsp = match kind_of_term t2 with
+  let (isevars,lsp) = match kind_of_term t2 with
     | Evar (n2,args2 as ev2)
         when not (Evd.is_defined isevars.evars n2) ->
 	if n1 = n2 then
@@ -518,8 +516,11 @@ let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) =
 	    evar_define env isevars ev1 t2
     | _ ->
 	evar_define env isevars ev1 t2 in
-  let pbs = get_changed_pb isevars lsp in
-  List.for_all (fun (pbty,t1,t2) -> conv_algo env isevars pbty t1 t2) pbs
+  let (isevars,pbs) = get_changed_pb isevars lsp in
+  List.fold_left
+    (fun (isevars,b as p) (pbty,t1,t2) ->
+      if b then conv_algo env isevars pbty t1 t2 else p) (isevars,true)
+    pbs
 
 (* Operations on value/type constraints *)
 
@@ -556,20 +557,21 @@ let mk_valcon c = Some c
 
 let refine_evar_as_arrow isevars ev =
   let (sigma,prod,evdom,evrng) = split_evar_to_arrow isevars.evars ev in
-  evars_reset_evd sigma isevars;
   let hst = evar_source (fst ev) isevars in
-  isevars.history <- (fst evrng,hst)::(fst evdom, hst)::isevars.history;
-  (prod,evdom,evrng)
+  let isevars' =
+    {isevars with
+     evars=sigma;
+     history = (fst evrng,hst)::(fst evdom, hst)::isevars.history } in
+  (isevars',prod,evdom,evrng)
 
 let define_evar_as_arrow isevars ev =
-  let (prod,_,_) = refine_evar_as_arrow isevars ev in
-  prod
+  let (isevars',prod,_,_) = refine_evar_as_arrow isevars ev in
+  isevars',prod
 
 let define_evar_as_sort isevars (ev,args) =
   let s = new_Type () in
   let sigma' = Evd.define isevars.evars ev s in
-  evars_reset_evd sigma' isevars;
-  destSort s
+  evars_reset_evd sigma' isevars, destSort s
 
 
 (* Propagation of constraints through application and abstraction:
@@ -578,15 +580,15 @@ let define_evar_as_sort isevars (ev,args) =
    an evar instantiate it with the product of 2 new evars. *)
 
 let split_tycon loc env isevars = function
-  | None -> Anonymous,None,None
+  | None -> isevars,(Anonymous,None,None)
   | Some c ->
       let sigma = evars_of isevars in
       let t = whd_betadeltaiota env sigma c in
       match kind_of_term t with
-        | Prod (na,dom,rng) -> na, Some dom, Some rng
+        | Prod (na,dom,rng) -> isevars, (na, Some dom, Some rng)
 	| Evar (n,_ as ev) when not (Evd.is_defined isevars.evars n) ->
-	    let (_,evdom,evrng) = refine_evar_as_arrow isevars ev in
-	    Anonymous, Some (mkEvar evdom), Some (mkEvar evrng)
+	    let (isevars',_,evdom,evrng) = refine_evar_as_arrow isevars ev in
+	    isevars',(Anonymous, Some (mkEvar evdom), Some (mkEvar evrng))
 	| _ -> error_not_product_loc loc env sigma c
 
 let valcon_of_tycon x = x
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index a08fb3f822..4223b0e782 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -52,14 +52,13 @@ val evars_of :  evar_defs ->  evar_map
 val non_instantiated : evar_map -> (evar * evar_info) list
 
 val create_evar_defs :  evar_map ->  evar_defs
-val evars_reset_evd :  evar_map ->  evar_defs -> unit
+val evars_reset_evd :  evar_map ->  evar_defs -> evar_defs
 val evar_source : existential_key -> evar_defs -> loc * hole_kind
 
 type evar_constraint = conv_pb * constr * constr
-val add_conv_pb :  evar_defs -> evar_constraint -> unit
+val add_conv_pb :  evar_constraint -> evar_defs -> evar_defs
 
 val is_defined_evar :  evar_defs -> existential -> bool
-val ise_try :  evar_defs -> (unit -> bool) list -> bool
 val ise_undefined :  evar_defs -> constr -> bool
 val has_undefined_isevars :  evar_defs -> constr -> bool
 
@@ -67,16 +66,21 @@ val new_isevar_sign :
  Environ.env -> Evd.evar_map -> Term.constr -> Term.constr list ->
   Evd.evar_map * Term.constr
 
-val new_isevar :  evar_defs -> env -> loc * hole_kind -> constr -> constr
+val new_isevar :  evar_defs -> env -> loc * hole_kind -> constr ->
+  evar_defs * constr
+
+(* the same with side-effects *)
+val e_new_isevar : evar_defs ref -> env -> loc * hole_kind -> constr -> constr
 
 val is_eliminator : constr -> bool
 val head_is_embedded_evar :  evar_defs -> constr -> bool
 val solve_simple_eqn :
-  (env ->  evar_defs -> conv_pb -> constr -> constr -> bool)
-  -> env ->  evar_defs -> conv_pb * existential * constr -> bool
+  (env ->  evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool)
+  -> env ->  evar_defs -> conv_pb * existential * constr ->
+    evar_defs * bool
 
-val define_evar_as_arrow : evar_defs -> existential -> types
-val define_evar_as_sort : evar_defs -> existential -> sorts
+val define_evar_as_arrow : evar_defs -> existential -> evar_defs * types
+val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts
 
 (* Value/Type constraints *)
 
@@ -95,7 +99,7 @@ val mk_valcon : constr -> val_constraint
 
 val split_tycon :
   loc -> env ->  evar_defs -> type_constraint -> 
-    name * type_constraint * type_constraint
+    evar_defs * (name * type_constraint * type_constraint)
 
 val valcon_of_tycon : type_constraint -> val_constraint
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index dcb30c4d00..d0402a552b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -32,6 +32,23 @@ open Pattern
 open Dyn
 
 
+let evd_comb0 f isevars =
+  let (evd',x) = f !isevars in
+  isevars := evd';
+  x
+let evd_comb1 f isevars x =
+  let (evd',y) = f !isevars x in
+  isevars := evd';
+  y
+let evd_comb2 f isevars x y =
+  let (evd',z) = f !isevars x y in
+  isevars := evd';
+  z
+let evd_comb3 f isevars x y z =
+  let (evd',t) = f !isevars x y z in
+  isevars := evd';
+  t
+
 (************************************************************************)
 (* This concerns Cases *)
 open Declarations
@@ -147,24 +164,23 @@ let evar_type_fixpoint loc env isevars lna lar vdefj =
   let lt = Array.length vdefj in 
     if Array.length lar = lt then 
       for i = 0 to lt-1 do 
-        if not (the_conv_x_leq env isevars
-		  (vdefj.(i)).uj_type
+        if not (e_cumul env isevars (vdefj.(i)).uj_type
 		  (lift lt lar.(i))) then
-          error_ill_typed_rec_body_loc loc env (evars_of isevars)
+          error_ill_typed_rec_body_loc loc env (evars_of !isevars)
             i lna vdefj lar
       done
 
 let check_branches_message loc env isevars c (explft,lft) = 
   for i = 0 to Array.length explft - 1 do
-    if not (the_conv_x_leq env isevars lft.(i) explft.(i)) then 
-      let sigma = evars_of isevars in
+    if not (e_cumul env isevars lft.(i) explft.(i)) then 
+      let sigma = evars_of !isevars 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
    | None -> j
-   | Some typ -> inh_conv_coerce_to loc env isevars j typ
+   | Some typ -> evd_comb2 (inh_conv_coerce_to loc env) isevars j typ
 
 let push_rels vars env = List.fold_right push_rel vars env
 
@@ -246,12 +262,12 @@ let rec pretype tycon env isevars lvar = function
   | REvar (loc, ev, instopt) ->
       (* Ne faudrait-il pas s'assurer que hyps est bien un
       sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
-      let hyps = (Evd.map (evars_of isevars) ev).evar_hyps in
+      let hyps = (Evd.map (evars_of !isevars) ev).evar_hyps in
       let args = match instopt with
         | None -> instance_from_named_context hyps
         | Some inst -> failwith "Evar subtitutions not implemented" in
       let c = mkEvar (ev, args) in
-      let j = (Retyping.get_judgment_of env (evars_of isevars) c) in
+      let j = (Retyping.get_judgment_of env (evars_of !isevars) c) in
       inh_conv_coerce_to_tycon loc env isevars j tycon
 
   | RPatVar (loc,(someta,n)) -> 
@@ -260,8 +276,8 @@ let rec pretype tycon env isevars lvar = function
   | RHole (loc,k) ->
       (match tycon with
 	 | Some ty ->
-	     { uj_val = new_isevar isevars env (loc,k) ty; uj_type = ty }
-	 | None -> error_unsolvable_implicit loc env (evars_of isevars) k)
+	     { uj_val = e_new_isevar isevars env (loc,k) ty; uj_type = ty }
+	 | None -> error_unsolvable_implicit loc env (evars_of !isevars) k)
 
   | RRec (loc,fixkind,names,bl,lar,vdef) ->
       let rec type_bl env ctxt = function
@@ -323,9 +339,9 @@ let rec pretype tycon env isevars lvar = function
 	| [] -> resj
 	| c::rest ->
 	    let argloc = loc_of_rawconstr c in
-	    let resj = inh_app_fun env isevars resj in
+	    let resj = evd_comb1 (inh_app_fun env) isevars resj in
             let resty =
-              whd_betadeltaiota env (evars_of isevars) resj.uj_type in
+              whd_betadeltaiota env (evars_of !isevars) 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
@@ -337,7 +353,7 @@ let rec pretype tycon env isevars lvar = function
 	      | _ ->
 		  let hj = pretype empty_tycon env isevars lvar c in
 		  error_cant_apply_not_functional_loc 
-		    (join_loc floc argloc) env (evars_of isevars)
+		    (join_loc floc argloc) env (evars_of !isevars)
 	      	    resj [hj]
 
       in let resj = apply_rec env 1 fj args in
@@ -356,7 +372,7 @@ let rec pretype tycon env isevars lvar = function
       inh_conv_coerce_to_tycon loc env isevars resj tycon
 
   | RLambda(loc,name,c1,c2)      ->
-      let (name',dom,rng) = split_tycon loc env isevars tycon in
+      let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon in
       let dom_valcon = valcon_of_tycon dom in
       let j = pretype_type dom_valcon env isevars lvar c1 in
       let var = (name,None,j.utj_val) in
@@ -385,10 +401,10 @@ let rec pretype tycon env isevars lvar = function
   | RLetTuple (loc,nal,(na,po),c,d) ->
       let cj = pretype empty_tycon env isevars lvar c in
       let (IndType (indf,realargs) as indt) = 
-	try find_rectype env (evars_of isevars) cj.uj_type
+	try find_rectype env (evars_of !isevars) cj.uj_type
 	with Not_found ->
 	  let cloc = loc_of_rawconstr c in
-	  error_case_not_inductive_loc cloc env (evars_of isevars) cj 
+	  error_case_not_inductive_loc cloc env (evars_of !isevars) cj 
       in
       let cstrs = get_constructors env indf in
       if Array.length cstrs <> 1 then
@@ -408,14 +424,14 @@ let rec pretype tycon env isevars lvar = function
 	 | Some p ->
              let env_p = push_rels psign env in
              let pj = pretype_type empty_valcon env_p isevars lvar p in
-             let ccl = nf_evar (evars_of isevars) pj.utj_val in
+             let ccl = nf_evar (evars_of !isevars) pj.utj_val in
 	     let psign = make_arity_signature env true indf in (* with names *)
 	     let p = it_mkLambda_or_LetIn ccl psign in
              let inst = 
 	       (Array.to_list cs.cs_concl_realargs)
 	       @[build_dependent_constructor cs] in
 	     let lp = lift cs.cs_nargs p in
-             let fty = hnf_lam_applist env (evars_of isevars) lp inst in
+             let fty = hnf_lam_applist env (evars_of !isevars) lp inst in
 	     let fj = pretype (mk_tycon fty) env_f isevars lvar d in
 	     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
 	     let v =
@@ -429,12 +445,12 @@ let rec pretype tycon env isevars lvar = function
              let tycon = option_app (lift cs.cs_nargs) tycon in
 	     let fj = pretype tycon env_f isevars lvar d in
 	     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
-	     let ccl = nf_evar (evars_of isevars) fj.uj_type in
+	     let ccl = nf_evar (evars_of !isevars) fj.uj_type in
              let ccl =
                if noccur_between 1 cs.cs_nargs ccl then
                  lift (- cs.cs_nargs) ccl 
                else
-                 error_cant_find_case_type_loc loc env (evars_of isevars) 
+                 error_cant_find_case_type_loc loc env (evars_of !isevars) 
                    cj.uj_val in
              let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
 	     let v =
@@ -448,10 +464,10 @@ let rec pretype tycon env isevars lvar = function
   | ROrderedCase (loc,st,po,c,[|f|],xx) when st <> MatchStyle ->
       let cj = pretype empty_tycon env isevars lvar c in
       let (IndType (indf,realargs) as indt) = 
-	try find_rectype env (evars_of isevars) cj.uj_type
+	try find_rectype env (evars_of !isevars) cj.uj_type
 	with Not_found ->
 	  let cloc = loc_of_rawconstr c in
-	  error_case_not_inductive_loc cloc env (evars_of isevars) cj 
+	  error_case_not_inductive_loc cloc env (evars_of !isevars) cj 
       in
       let j = match po with
 	 | Some p ->
@@ -459,16 +475,16 @@ let rec pretype tycon env isevars lvar = function
              let dep = is_dependent_elimination env pj.uj_type indf in
              let ar =
                arity_of_case_predicate env indf dep (Type (new_univ())) in
-             let _ = the_conv_x_leq env isevars pj.uj_type ar in
-	     let pj = j_nf_evar (evars_of isevars) pj in
+             let _ = e_cumul env isevars pj.uj_type ar in
+	     let pj = j_nf_evar (evars_of !isevars) pj in
 	     let pj = if dep then pj else make_dep_of_undep env indt pj in
 	     let (bty,rsty) = 
 	       Indrec.type_rec_branches 
-		 false env (evars_of isevars) indt pj.uj_val cj.uj_val 
+		 false env (evars_of !isevars) indt pj.uj_val cj.uj_val 
 	     in
 	     if Array.length bty <> 1 then
 	       error_number_branches_loc 
-		 loc env (evars_of isevars) cj (Array.length bty);
+		 loc env (evars_of !isevars) cj (Array.length bty);
 	     let fj = 
 	       let tyc = bty.(0) in 
 	       pretype (mk_tycon tyc) env isevars lvar f 
@@ -487,7 +503,7 @@ let rec pretype tycon env isevars lvar = function
              (* get type information from type of branches *)
 	     let expbr = Cases.branch_scheme env isevars false indf in
 	     if Array.length expbr <> 1 then
-	       error_number_branches_loc loc env (evars_of isevars) 
+	       error_number_branches_loc loc env (evars_of !isevars) 
 		 cj (Array.length expbr);
              let expti = expbr.(0) in
 	     let fj = pretype (mk_tycon expti) env isevars lvar f in
@@ -500,32 +516,32 @@ let rec pretype tycon env isevars lvar = function
 		     let arsgn = make_arity_signature env true indf in
                      let pred = lift (List.length arsgn) pred in
   		     let pred = 
-                       it_mkLambda_or_LetIn (nf_evar (evars_of isevars) pred)
+                       it_mkLambda_or_LetIn (nf_evar (evars_of !isevars) pred)
 			 arsgn in
                      false, pred
 	         | None ->
-                     let sigma = evars_of isevars in
+                     let sigma = evars_of !isevars in
                      error_cant_find_case_type_loc loc env sigma cj.uj_val
 	     in
              let ok, p =
 	       try
 		 let pred = 
 		   Cases.pred_case_ml 
-		     env (evars_of isevars) false indt (0,fj.uj_type) 
+		     env (evars_of !isevars) false indt (0,fj.uj_type) 
 		 in 
-		 if has_undefined_isevars isevars pred then
+		 if has_undefined_isevars !isevars pred then
 		   use_constraint ()
 		 else
 		   true, pred
 	       with Cases.NotInferable _ ->
 		 use_constraint ()
 	     in 
-	     let p = nf_evar (evars_of isevars) p in
+	     let p = nf_evar (evars_of !isevars) p in
 	     let (bty,rsty) =
 	       Indrec.type_rec_branches
-		 false env (evars_of isevars) indt p cj.uj_val 
+		 false env (evars_of !isevars) indt p cj.uj_val 
 	     in
-	     let _ = option_app (the_conv_x_leq env isevars rsty) tycon in
+	     let _ = option_app (e_cumul env isevars rsty) tycon in
 	     let fj = 
 	       if ok then fj 
 	       else pretype (mk_tycon bty.(0)) env isevars lvar f 
@@ -643,10 +659,10 @@ let rec pretype tycon env isevars lvar = function
   | RIf (loc,c,(na,po),b1,b2) ->
       let cj = pretype empty_tycon env isevars lvar c in
       let (IndType (indf,realargs) as indt) = 
-	try find_rectype env (evars_of isevars) cj.uj_type
+	try find_rectype env (evars_of !isevars) cj.uj_type
 	with Not_found ->
 	  let cloc = loc_of_rawconstr c in
-	  error_case_not_inductive_loc cloc env (evars_of isevars) cj in
+	  error_case_not_inductive_loc cloc env (evars_of !isevars) cj in
       let cstrs = get_constructors env indf in 
       if Array.length cstrs <> 2 then
         user_err_loc (loc,"",
@@ -661,13 +677,13 @@ let rec pretype tycon env isevars lvar = function
 	| Some p ->
 	    let env_p = push_rels psign env in
             let pj = pretype_type empty_valcon env_p isevars lvar p in
-            let ccl = nf_evar (evars_of isevars) pj.utj_val in
+            let ccl = nf_evar (evars_of !isevars) pj.utj_val in
 	    let pred = it_mkLambda_or_LetIn ccl psign in
 	    pred, lift (- nar) (beta_applist (pred,[cj.uj_val]))
 	| None -> 
 	    let p = match tycon with
 	    | Some ty -> ty
-	    | None -> new_isevar isevars env (loc,InternalHole) (new_Type ())
+	    | None -> e_new_isevar isevars env (loc,InternalHole) (new_Type ())
 	    in
 	    it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
       let f cs b =
@@ -680,8 +696,8 @@ let rec pretype tycon env isevars lvar = function
 	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
-      let pred = nf_evar (evars_of isevars) pred in
-      let p = nf_evar (evars_of isevars) p in
+      let pred = nf_evar (evars_of !isevars) pred in
+      let p = nf_evar (evars_of !isevars) p in
       let v =
 	let mis,_ = dest_ind_family indf in
 	let ci = make_default_case_info env IfStyle mis in
@@ -693,17 +709,17 @@ let rec pretype tycon env isevars lvar = function
       let isrec = (st = MatchStyle) in
       let cj = pretype empty_tycon env isevars lvar c in
       let (IndType (indf,realargs) as indt) = 
-	try find_rectype env (evars_of isevars) cj.uj_type
+	try find_rectype env (evars_of !isevars) cj.uj_type
 	with Not_found ->
 	  let cloc = loc_of_rawconstr c in
-	  error_case_not_inductive_loc cloc env (evars_of isevars) cj in
+	  error_case_not_inductive_loc cloc env (evars_of !isevars) cj in
       let (dep,pj) = match po with
 	| Some p ->
             let pj = pretype empty_tycon env isevars lvar p in
             let dep = is_dependent_elimination env pj.uj_type indf in
             let ar =
               arity_of_case_predicate env indf dep (Type (new_univ())) in
-            let _ = the_conv_x_leq env isevars pj.uj_type ar in
+            let _ = e_cumul env isevars pj.uj_type ar in
             (dep, pj)
 	| None -> 
             (* get type information from type of branches *)
@@ -719,12 +735,12 @@ let rec pretype tycon env isevars lvar = function
 		      let arsgn = make_arity_signature env true indf in
                       let pred = lift (List.length arsgn) pred in
   		      let pred = 
-			it_mkLambda_or_LetIn (nf_evar (evars_of isevars) pred)
+			it_mkLambda_or_LetIn (nf_evar (evars_of !isevars) pred)
 			  arsgn in
                       (true, 
-                       Retyping.get_judgment_of env (evars_of isevars) pred)
+                       Retyping.get_judgment_of env (evars_of !isevars) pred)
 	          | None ->
-                      let sigma = evars_of isevars in
+                      let sigma = evars_of !isevars in
                       error_cant_find_case_type_loc loc env sigma cj.uj_val
 	      else
 		try
@@ -733,11 +749,11 @@ let rec pretype tycon env isevars lvar = function
 		    pretype (mk_tycon expti) env isevars lvar lf.(i) in
 		  let pred = 
 		    Cases.pred_case_ml (* eta-expanse *)
-                      env (evars_of isevars) isrec indt (i,fj.uj_type) in
-		  if has_undefined_isevars isevars pred then findtype (i+1)
+                      env (evars_of !isevars) isrec indt (i,fj.uj_type) in
+		  if has_undefined_isevars !isevars pred then findtype (i+1)
 		  else 
 		    let pty =
-                      Retyping.get_type_of env (evars_of isevars) pred in
+                      Retyping.get_type_of env (evars_of !isevars) pred in
 		    let pj = { uj_val = pred; uj_type = pty } in
 (*
                     let _ = option_app (the_conv_x_leq env isevars pred) tycon
@@ -747,14 +763,14 @@ let rec pretype tycon env isevars lvar = function
 		with Cases.NotInferable _ -> findtype (i+1) in
 	    findtype 0 
       in
-      let pj = j_nf_evar (evars_of isevars) pj in
+      let pj = j_nf_evar (evars_of !isevars) pj in
       let pj = if dep then pj else make_dep_of_undep env indt pj in
       let (bty,rsty) =
 	Indrec.type_rec_branches
-          isrec env (evars_of isevars) indt pj.uj_val cj.uj_val in
-      let _ = option_app (the_conv_x_leq env isevars rsty) tycon in
+          isrec env (evars_of !isevars) indt pj.uj_val cj.uj_val in
+      let _ = option_app (e_cumul env isevars rsty) tycon in
       if Array.length bty <> Array.length lf then
-	error_number_branches_loc loc env (evars_of isevars) 
+	error_number_branches_loc loc env (evars_of !isevars) 
 	  cj (Array.length bty)
       else
 	let lfj =
@@ -767,7 +783,7 @@ let rec pretype tycon env isevars lvar = function
 	let v =
 	  if isrec
 	  then 
-	    transform_rec loc env (evars_of isevars)(pj,cj.uj_val,lfv) indt
+	    transform_rec loc env (evars_of !isevars)(pj,cj.uj_val,lfv) indt
 	  else
 	    let mis,_ = dest_ind_family indf in
 	    let ci = make_default_case_info env st mis in
@@ -785,7 +801,7 @@ let rec pretype tycon env isevars lvar = function
           if isrec && mis_is_recursive_subset [tyi] recargs then
             Some (Detyping.detype (false,env)
 	      (ids_of_context env) (names_of_rel_context env)
-              (nf_evar (evars_of isevars) v))
+              (nf_evar (evars_of !isevars) v))
 	  else
 	    (* Translate into a "match ... with" *)
             let rtntypopt, indnalopt = match po with
@@ -902,7 +918,7 @@ let rec pretype tycon env isevars lvar = function
   | 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 !isevars) c) in
       j
       (*inh_conv_coerce_to_tycon loc env isevars j tycon*)
     else
@@ -914,39 +930,39 @@ and pretype_type valcon env isevars lvar = function
       (match valcon with
 	 | Some v ->
              let s =
-               let sigma = evars_of isevars in
+               let sigma = evars_of !isevars in
                let t = Retyping.get_type_of env sigma v in
                match kind_of_term (whd_betadeltaiota env sigma t) with
                  | Sort s -> s
                  | Evar v when is_Type (existential_type sigma v) -> 
-                     define_evar_as_sort isevars v
+                     evd_comb1 (define_evar_as_sort) isevars v
                  | _ -> 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 = new_isevar isevars env loc (mkSort s);
+	     { utj_val = e_new_isevar isevars env loc (mkSort s);
 	       utj_type = s})
   | c ->
       let j = pretype empty_tycon env isevars lvar c in
-      let tj = inh_coerce_to_sort env isevars j in
+      let tj = evd_comb1 (inh_coerce_to_sort env) isevars j in
       match valcon with
 	| None -> tj
 	| Some v ->
-	    if the_conv_x_leq env isevars v tj.utj_val then tj
+	    if e_cumul env isevars v tj.utj_val then tj
 	    else
 	      error_unexpected_type_loc
-                (loc_of_rawconstr c) env (evars_of isevars) tj.utj_val v
+                (loc_of_rawconstr c) env (evars_of !isevars) tj.utj_val v
 
 
 let unsafe_infer tycon isevars env lvar constr =
   let j = pretype tycon env isevars lvar constr in
-  j_nf_evar (evars_of isevars) j
+  j_nf_evar (evars_of !isevars) j
 
 let unsafe_infer_type valcon isevars env lvar constr =
   let tj = pretype_type valcon env isevars lvar constr in
-  tj_nf_evar (evars_of isevars) tj
+  tj_nf_evar (evars_of !isevars) tj
 
 (* If fail_evar is false, [process_evars] builds a meta_map with the
    unresolved Evar that were not in initial sigma; otherwise it fail
@@ -958,14 +974,14 @@ let unsafe_infer_type valcon isevars env lvar constr =
 (* assumes the defined existentials have been replaced in c (should be
    done in unsafe_infer and unsafe_infer_type) *)
 let check_evars fail_evar env initial_sigma isevars c =
-  let sigma = evars_of isevars in
+  let sigma = evars_of !isevars in
   let rec proc_rec c =
     match kind_of_term c with
       | Evar (ev,args as k) ->
           assert (Evd.in_dom sigma ev);
 	  if not (Evd.in_dom initial_sigma ev) then
 	    (if fail_evar then
-              let (loc,k) = evar_source ev isevars in
+              let (loc,k) = evar_source ev !isevars in
 	       error_unsolvable_implicit loc env sigma k)
       | _ -> iter_constr proc_rec c      
   in
@@ -980,10 +996,10 @@ let check_evars fail_evar env initial_sigma isevars c =
 type open_constr = evar_map * constr
 
 let ise_resolve_casted_gen fail_evar sigma env lvar typ c =
-  let isevars = create_evar_defs sigma in
+  let isevars = ref (create_evar_defs sigma) in
   let j = unsafe_infer (mk_tycon typ) isevars env lvar c in
   check_evars fail_evar env sigma isevars (mkCast(j.uj_val,j.uj_type));
-  (evars_of isevars, j)
+  (evars_of !isevars, j)
 
 let ise_resolve_casted sigma env typ c =
   ise_resolve_casted_gen true sigma env ([],[]) typ c
@@ -993,16 +1009,16 @@ let ise_resolve_casted sigma env typ c =
    allows us to extend env with some bindings *)
 let ise_infer_gen fail_evar sigma env lvar exptyp c =
   let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
-  let isevars = create_evar_defs sigma in
+  let isevars = ref (create_evar_defs sigma) in
   let j = unsafe_infer tycon isevars env lvar c in
   check_evars fail_evar env sigma isevars (mkCast(j.uj_val,j.uj_type));
-  (evars_of isevars, j)
+  (evars_of !isevars, j)
 
 let ise_infer_type_gen fail_evar sigma env lvar c =
-  let isevars = create_evar_defs sigma in
+  let isevars = ref (create_evar_defs sigma) in
   let tj = unsafe_infer_type empty_valcon isevars env lvar c in
   check_evars fail_evar env sigma isevars tj.utj_val;
-  (evars_of isevars, tj)
+  (evars_of !isevars, tj)
 
 type var_map = (identifier * unsafe_judgment) list
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 3d88422eb0..57a3d1be89 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -71,12 +71,12 @@ val constr_out : Dyn.t -> constr
  * Unused outside, but useful for debugging
  *)
 val pretype : 
-  type_constraint -> env -> evar_defs -> 
+  type_constraint -> env -> evar_defs ref -> 
     var_map * (identifier * identifier option) list ->
     rawconstr -> unsafe_judgment
 
 val pretype_type : 
-  val_constraint -> env -> evar_defs ->
+  val_constraint -> env -> evar_defs ref ->
     var_map * (identifier * identifier option) list ->
     rawconstr -> unsafe_type_judgment
 (*i*)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index aea164a9bf..83377449dd 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -49,7 +49,7 @@ let abstract_list_all env sigma typ c l =
 
 (*******************************)
 
-type maps = evar_map * meta_map
+type maps = evar_defs * meta_map
 
 (* [w_Define evd sp c]
  *
@@ -59,18 +59,22 @@ type maps = evar_map * meta_map
  * No unification is performed in order to assert that [c] has the
  * correct type.
  *)
-let w_Define sp c evd =
+let w_Define sp c (evd,mmap) =
   let sigma = evars_of evd in
   if Evd.is_defined sigma sp then
     error "Unify.w_Define: cannot define evar twice";
   let spdecl = Evd.map sigma sp in
   let env = evar_env spdecl in
   let _ =
-    try Typing.check env (Evd.rmv sigma sp) c spdecl.evar_concl
-    with Not_found ->
-      error "Instantiation contains unlegal variables" in
+    try Typing.mcheck env (Evd.rmv sigma sp,Metamap.empty) c spdecl.evar_concl
+    with
+	Not_found -> error "Instantiation contains unlegal variables"
+      | (Type_errors.TypeError (e, Type_errors.UnboundVar v))-> 
+      errorlabstrm "w_Define"
+      (str "Cannot use variable " ++ pr_id v ++ str " to define " ++ 
+       str (string_of_existential sp)) in
   let spdecl' = { spdecl with evar_body = Evar_defined c } in
-  evars_reset_evd (Evd.add sigma sp spdecl') evd
+  (evars_reset_evd (Evd.add sigma sp spdecl') evd, mmap)
 
 
 (* Unification à l'ordre 0 de m et n: [unify_0 env sigma cv_pb m n]
@@ -194,21 +198,20 @@ let unify_0 env sigma cv_pb m n =
  * close it off.  But this might not always work,
  * since other metavars might also need to be resolved. *)
 
-let applyHead env sigma n c  = 
-  let evd = create_evar_defs sigma in
-  let rec apprec n c cty =
+let applyHead env evd n c  = 
+  let rec apprec n c cty evd =
     if n = 0 then 
-      (evars_of evd, c)
+      (evd, c)
     else 
       match kind_of_term (whd_betadeltaiota env (evars_of evd) cty) with
         | Prod (_,c1,c2) ->
-            let evar =
+            let (evd',evar) =
               Evarutil.new_isevar evd env
                 (dummy_loc,Rawterm.InternalHole) c1 in
-	    apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2)
+	    apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd'
 	| _ -> error "Apply_Head_Then"
   in 
-  apprec n c (Typing.type_of env (evars_of evd) c)
+  apprec n c (Typing.type_of env (evars_of evd) c) evd
 
 let is_mimick_head f =
   match kind_of_term f with
@@ -219,19 +222,17 @@ let is_mimick_head f =
    or in evars, possibly generating new unification problems; if [b]
    is true, unification of types of metas is required *)
 
-let w_merge env with_types metas evars (sigma,metamap) =
-  let evd = create_evar_defs sigma in
-  let mmap = ref metamap in
+let w_merge env with_types metas evars maps =
   let ty_metas = ref [] in
   let ty_evars = ref [] in
-  let rec w_merge_rec metas evars =
+  let rec w_merge_rec (evd,mmap as maps) metas evars =
     match (evars,metas) with
-      | ([], []) -> ()
+      | ([], []) -> maps
 
       | ((lhs,rhs)::t, metas) ->
       (match kind_of_term rhs with
 
-	| Meta k -> w_merge_rec ((k,lhs)::metas) t
+	| Meta k -> w_merge_rec maps ((k,lhs)::metas) t
 
 	| krhs ->
         (match kind_of_term lhs with
@@ -240,7 +241,7 @@ let w_merge env with_types metas evars (sigma,metamap) =
     	      if is_defined_evar evd ev then
 		let (metas',evars') =
                   unify_0 env (evars_of evd) CONV rhs lhs in
-		w_merge_rec (metas'@metas) (evars'@t)
+		w_merge_rec maps (metas'@metas) (evars'@t)
     	      else begin
 		let rhs' = 
 		  if occur_meta rhs then subst_meta metas rhs else rhs 
@@ -250,60 +251,59 @@ let w_merge env with_types metas evars (sigma,metamap) =
                 match krhs with
 		  | App (f,cl) when is_mimick_head f ->
 		      (try 
-                        w_Define evn rhs' evd; 
-		        w_merge_rec metas t
+		        w_merge_rec (w_Define evn rhs' maps) metas t
 		      with ex when precatchable_exception ex ->
-                        mimick_evar f (Array.length cl) evn;
-			w_merge_rec metas evars)
+                        let maps' =
+                          mimick_evar maps f (Array.length cl) evn in
+			w_merge_rec maps' metas evars)
                   | _ ->
                       (* ensure tail recursion in non-mimickable case! *)
-                      w_Define evn rhs' evd; 
-		      w_merge_rec metas t
+		      w_merge_rec (w_Define evn rhs' maps) metas t
 	      end
 
 	  | _ -> anomaly "w_merge_rec"))
 
       | ([], (mv,n)::t) ->
-    	  if meta_defined !mmap mv then
+    	  if meta_defined mmap mv then
             let (metas',evars') =
-              unify_0 env (evars_of evd) CONV (meta_fvalue !mmap mv).rebus n in
-            w_merge_rec (metas'@t) evars'
+              unify_0 env (evars_of evd) CONV (meta_fvalue mmap mv).rebus n in
+            w_merge_rec maps (metas'@t) evars'
     	  else
             begin
 	      if with_types (* or occur_meta mvty *) then
-	        (let mvty = meta_type !mmap mv in
+	        (let mvty = meta_type mmap mv in
 		try 
                   let sigma = evars_of evd in
                   (* why not typing with the metamap ? *)
-		  let nty = Typing.type_of env sigma (nf_meta !mmap n) in
+		  let nty = Typing.type_of env sigma (nf_meta mmap n) in
 		  let (mc,ec) = unify_0 env sigma CUMUL nty mvty in
                   ty_metas := mc @ !ty_metas;
                   ty_evars := ec @ !ty_evars
 		with e when precatchable_exception e -> ());
-              mmap := meta_assign mv n !mmap;
-	      w_merge_rec t []
+              let mmap' = meta_assign mv n mmap in
+	      w_merge_rec (evd,mmap') t []
             end
-  and mimick_evar hdc nargs sp =
+
+  and mimick_evar (evd,mmap) hdc nargs sp =
     let ev = Evd.map (evars_of evd) sp in
     let sp_env = Global.env_of_context ev.evar_hyps in
-    let (sigma', c) = applyHead sp_env (evars_of evd) nargs hdc in
-    evars_reset_evd sigma' evd;
+    let (evd', c) = applyHead sp_env evd nargs hdc in
     let (mc,ec) =
-      unify_0 sp_env (evars_of evd) CUMUL
-        (Retyping.get_type_of sp_env (evars_of evd) c) ev.evar_concl in
-    w_merge_rec mc ec;
-    if sigma'== (evars_of evd)
-    then w_Define sp c evd
-    else w_Define sp (Evarutil.nf_evar (evars_of evd) c) evd in
+      unify_0 sp_env (evars_of evd') CUMUL
+        (Retyping.get_type_of sp_env (evars_of evd') c) ev.evar_concl in
+    let maps' = w_merge_rec (evd',mmap) mc ec in
+    if (evars_of evd') == (evars_of (fst maps'))
+    then w_Define sp c maps'
+    else w_Define sp (Evarutil.nf_evar (evars_of (fst maps')) c) maps' in
 
   (* merge constraints *)
-  w_merge_rec metas evars;
-  (if with_types then
+  let maps' = w_merge_rec maps metas evars in
+  if with_types then
     (* merge constraints about types: if they fail, don't worry *)
-    try w_merge_rec !ty_metas !ty_evars
-(* TODO: should backtrack *)
-    with e when precatchable_exception e -> ());
-  (evars_of evd, !mmap)
+    try w_merge_rec maps' !ty_metas !ty_evars
+    with e when precatchable_exception e -> maps'
+  else
+    maps'
 
 (* [w_unify env evd M N]
    performs a unification of M and N, generating a bunch of
@@ -316,7 +316,7 @@ let w_merge env with_types metas evars (sigma,metamap) =
    types of metavars are unifiable with the types of their instances    *)
 
 let w_unify_core_0 env with_types cv_pb m n evd =
-  let (mc,ec) = unify_0 env (fst evd) cv_pb m n in 
+  let (mc,ec) = unify_0 env (evars_of (fst evd)) cv_pb m n in 
   w_merge env with_types mc ec evd
 
 let w_unify_0 env = w_unify_core_0 env false
@@ -419,7 +419,7 @@ let w_unify_to_subterm_list env allow_K oplist t evd =
     (evd,[])
 
 let secondOrderAbstraction env allow_K typ (p, oplist) evd =
-  let sigma = fst evd in
+  let sigma = evars_of (fst evd) in
   let (evd',cllist) =
     w_unify_to_subterm_list env allow_K oplist typ evd in
   let typp = meta_type (snd evd') p in
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index d05b8cb5a8..f033c9e87f 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -15,11 +15,12 @@ open Term
 open Sign
 open Environ
 open Evd
+open Evarutil
 (*i*)
 
-type maps = evar_map * meta_map
+type maps = evar_defs * meta_map
 
-val w_Define : evar -> constr -> Evarutil.evar_defs -> unit
+val w_Define : evar -> constr -> maps -> maps
 
 (* The "unique" unification fonction *)
 val w_unify :