amelioration de la structure des univers

elimination des compteurs globaux de metas et d'evars du noyau
nettoyage de safe_typing.ml (plus de flags)


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

7 files changed, 220 insertions, 189 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 3e530b6720..14a4a24f2d 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -771,7 +771,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) !isevars) p) pv in
+  let pv'= Array.map (fun (n,sign,_,p) -> n,splay_constr (whd_betaiotaevar (push_rels (List.rev sign) env) (evars_of isevars)) p) pv in
   let n1,op1 = let (n1,(op1,args1)) = pv'.(0) in n1,op1 in
   if Array.for_all (fun (ni,(opi,_)) -> eq_operator_lift k (n1,ni) (op1,opi)) pv'
   then
@@ -802,7 +802,7 @@ let infer_predicate env isevars typs cstrs (IndFamily (mis,_) as indf) =
       let pred = it_mkLambda_or_LetIn (lift (List.length sign) typn) sign in
       (true,pred) (* true = dependent -- par défaut *)
     else
-      let s = get_sort_of env !isevars typs.(0) in
+      let s = get_sort_of env (evars_of isevars) typs.(0) in
       let predpred = it_mkLambda_or_LetIn (mkSort s) sign in
       let caseinfo = make_default_case_info mis in
       let brs = array_map2 abstract_conclusion typs cstrs in
@@ -933,7 +933,7 @@ let specialize_predicate_match tomatchs cs = function
 let find_predicate env isevars p typs cstrs current (IndType (indf,realargs)) =
   let (dep,pred) =
     match p with
-      | Some p -> abstract_predicate env !isevars indf p
+      | Some p -> abstract_predicate env (evars_of isevars) indf p
       | None -> infer_predicate env isevars typs cstrs indf in
   let typ = whd_beta (applist (pred, realargs)) in
   if dep then
@@ -1021,7 +1021,7 @@ let build_branch current pb eqns const_info =
     List.fold_right
       (fun (na,t) (env,typs) ->
  	 (push_rel_assum (na,t) env,
-	  ((na,to_mutind env !(pb.isevars) t),t)::typs))
+	  ((na,to_mutind env (evars_of (pb.isevars)) t),t)::typs))
       typs (pb.env,[]) in
   let tomatchs =
     List.fold_left2
@@ -1123,7 +1123,8 @@ and compile_further pb firstnext rest =
 
 and compile_aliases pb =
   let aliases, history = simplify_history pb.history in
-  let sign, newenv, mat = insert_aliases pb.env !(pb.isevars) aliases pb.mat in
+  let sign, newenv, mat =
+    insert_aliases pb.env (evars_of pb.isevars) aliases pb.mat in
   let n = List.length sign in
   let pb =
     {pb with
@@ -1249,7 +1250,7 @@ exception NotCoercible
 
 let inh_coerce_to_ind isevars env ty tyi =
   let (ntys,_) =
-    splay_prod env !isevars (mis_arity (Global.lookup_mind_specif tyi)) in
+    splay_prod env (evars_of isevars) (mis_arity (Global.lookup_mind_specif tyi)) in
    let (_,evarl) =
     List.fold_right
       (fun (na,ty) (env,evl) ->
@@ -1271,18 +1272,18 @@ let coerce_row typing_fun isevars env cstropt tomatch =
 	  (let tyi = inductive_of_rawconstructor c in
 	   try 
 	     let indtyp = inh_coerce_to_ind isevars env typ tyi in
-	     IsInd (typ,find_rectype env !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
-	       let mind,_ = find_mrectype env !isevars typ in
+	       let mind,_ = find_mrectype env (evars_of isevars) typ in
 	       error_bad_constructor_loc cloc
 		 (constructor_of_rawconstructor c) mind
 	     with Induc ->
 	       error_case_not_inductive_loc
 		 (loc_of_rawconstr tomatch) CCI env j.uj_val typ)
       | None -> 
-	  try IsInd (typ,find_rectype env !isevars typ)
+	  try IsInd (typ,find_rectype env (evars_of isevars) typ)
 	  with Induc -> NotInd typ
   in (j.uj_val,t)
 
@@ -1369,21 +1370,21 @@ let prepare_predicate typing_fun isevars env tomatchs = function
   | Some pred ->
       let loc = loc_of_rawconstr pred in
       let dep, predj =
-	let isevars_copy = ref !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, typing_fun (mk_tycon ndep_arity) env pred
 	with PretypeError _ | TypeError _ |
 	    Stdpp.Exc_located (_,(PretypeError _ | TypeError _)) ->
-        isevars := !isevars_copy;
+        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, typing_fun (mk_tycon dep_arity) env pred
 	with PretypeError _ | TypeError _ |
 	  Stdpp.Exc_located (_,(PretypeError _ | TypeError _)) ->
-        isevars := !isevars_copy;
+        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 *)
@@ -1392,9 +1393,9 @@ let prepare_predicate typing_fun isevars env tomatchs = function
 	  loc env predj.uj_val ndep_arity dep_arity
       in
 (*
-      let etapred,cdep = case_dependent env !isevars loc predj tomatchs in
+      let etapred,cdep = case_dependent env (evars_of isevars) loc predj tomatchs in
 *)
-      Some (build_initial_predicate env !isevars dep predj.uj_val tomatchs)
+      Some (build_initial_predicate env (evars_of isevars) dep predj.uj_val tomatchs)
 
 
 (**************************************************************************)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 5f8e90cb29..3e5e064bca 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -16,6 +16,7 @@ open Typeops
 open Pretype_errors
 open Classops
 open Recordops
+open Evarutil
 open Evarconv
 open Retyping
 
@@ -68,37 +69,37 @@ let apply_coercion env p hj typ_cl =
   with _ -> anomaly "apply_coercion"
 
 let inh_app_fun env isevars j = 
-  let t = whd_betadeltaiota env !isevars j.uj_type in
+  let t = whd_betadeltaiota env (evars_of isevars) j.uj_type in
   match kind_of_term t with
     | IsProd (_,_,_) -> j
     | _ ->
        	(try
- 	   let t,i1 = class_of1 env !isevars j.uj_type in
+ 	   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)
 
 let inh_tosort_force env isevars j =
   try
-    let t,i1 = class_of1 env !isevars j.uj_type in
+    let t,i1 = class_of1 env (evars_of isevars) j.uj_type in
     let p = lookup_path_to_sort_from i1 in
     apply_coercion env p j t 
   with Not_found -> 
     j
 
 let inh_coerce_to_sort env isevars j =
-  let typ = whd_betadeltaiota env !isevars j.uj_type in
+  let typ = whd_betadeltaiota env (evars_of isevars) j.uj_type in
   match kind_of_term typ with
     | IsSort s -> { utj_val = j.uj_val; utj_type = s }
     | _ ->
         let j1 = inh_tosort_force env isevars j in 
-	type_judgment env !isevars j1 
+	type_judgment env (evars_of isevars) j1 
 
 let inh_coerce_to_fail env isevars c1 hj =
   let hj' =
     try 
-      let t1,i1 = class_of1 env !isevars c1 in
-      let t2,i2 = class_of1 env !isevars hj.uj_type in
+      let t1,i1 = class_of1 env (evars_of isevars) c1 in
+      let t2,i2 = class_of1 env (evars_of isevars) hj.uj_type in
       let p = lookup_path_between (i2,i1) in
       apply_coercion env p hj t2
     with Not_found -> raise NoCoercion 
@@ -115,10 +116,10 @@ let rec inh_conv_coerce_to_fail env isevars c1 hj =
     try 
       inh_coerce_to_fail env isevars c1 hj
     with NoCoercion ->  (* try ... with _ -> ... is BAD *)
-      (match kind_of_term (whd_betadeltaiota env !isevars t),
-	     kind_of_term (whd_betadeltaiota env !isevars c1) with
+      (match kind_of_term (whd_betadeltaiota env (evars_of isevars) t),
+	     kind_of_term (whd_betadeltaiota env (evars_of isevars) c1) with
 	 | IsProd (_,t1,t2), IsProd (name,u1,u2) -> 
-             let v' = whd_betadeltaiota env !isevars v in
+             let v' = whd_betadeltaiota env (evars_of isevars) v in
              if (match kind_of_term v' with
                    | IsLambda (_,v1,v2) ->
                        the_conv_x env isevars v1 u1 (* leq v1 u1? *)
@@ -128,7 +129,7 @@ let rec inh_conv_coerce_to_fail env isevars c1 hj =
                let env1 = push_rel_assum (x,v1) env in
                let h2 = inh_conv_coerce_to_fail env1 isevars u2
 			  {uj_val = v2; uj_type = t2 } in
-               fst (abs_rel env !isevars x v1 h2)
+               fst (abs_rel env (evars_of isevars) x v1 h2)
              else 
                let name = (match name with 
 			     | Anonymous -> Name (id_of_string "x")
@@ -142,7 +143,7 @@ let rec inh_conv_coerce_to_fail env isevars c1 hj =
 			 { uj_val = mkApp (lift 1 v, [|h1.uj_val|]);
                            uj_type = subst1 h1.uj_val t2 }
 	       in
-	       fst (abs_rel env !isevars name u1 h2)
+	       fst (abs_rel env (evars_of isevars) name u1 h2)
 	 | _ -> raise NoCoercion)
 
 let inh_conv_coerce_to loc env isevars cj t =
@@ -150,8 +151,8 @@ let inh_conv_coerce_to loc env isevars cj t =
     try 
       inh_conv_coerce_to_fail env isevars t cj 
     with NoCoercion -> 
-      let rcj = j_nf_ise env !isevars cj in
-      let at = nf_ise1 !isevars t in
+      let rcj = j_nf_ise env (evars_of isevars) cj in
+      let at = nf_ise1 (evars_of isevars) t in
       error_actual_type_loc loc env rcj.uj_val rcj.uj_type at
   in
   { uj_val = cj'.uj_val; uj_type = t }
@@ -165,7 +166,8 @@ let inh_apply_rel_list apploc env isevars argjl (funloc,funj) tycon =
     | [] -> resj
     | (loc,hj)::restjl ->
 	let resj = inh_app_fun env isevars resj in
-      	match kind_of_term (whd_betadeltaiota env !isevars resj.uj_type) with
+        let ntyp = whd_betadeltaiota env (evars_of isevars) resj.uj_type in
+      	match kind_of_term ntyp with
           | IsProd (na,c1,c2) ->
               let hj' =
 		try 
@@ -173,16 +175,16 @@ let inh_apply_rel_list apploc env isevars argjl (funloc,funj) tycon =
 		with NoCoercion ->
 (*
                   error_cant_apply_bad_type_loc apploc env 
-		    (n,nf_ise1 !isevars c1,
-		     nf_ise1 !isevars hj.uj_type)
-		    (j_nf_ise env !isevars funj)
-		    (jl_nf_ise env !isevars argjl) in
+		    (n,nf_ise1 (evars_of isevars) c1,
+		     nf_ise1 (evars_of isevars) hj.uj_type)
+		    (j_nf_ise env (evars_of isevars) funj)
+		    (jl_nf_ise env (evars_of isevars) argjl) in
 *)
                   error_cant_apply_bad_type_loc apploc env 
-		    (1,nf_ise1 !isevars c1,
-		     nf_ise1 !isevars hj.uj_type)
-		    (j_nf_ise env !isevars resj)
-		    (jl_nf_ise env !isevars (List.map snd restjl)) in
+		    (1,nf_ise1 (evars_of isevars) c1,
+		     nf_ise1 (evars_of isevars) hj.uj_type)
+		    (j_nf_ise env (evars_of isevars) resj)
+		    (jl_nf_ise env (evars_of isevars) (List.map snd restjl)) in
 	      let newresj =
       		{ uj_val = applist (j_val resj, [j_val hj']);
 		  uj_type = subst1 hj'.uj_val c2 } in
@@ -190,12 +192,13 @@ let inh_apply_rel_list apploc env isevars argjl (funloc,funj) tycon =
           | _ ->
 (*
               error_cant_apply_not_functional_loc apploc env
-	      	(j_nf_ise env !isevars funj) (jl_nf_ise env !isevars argjl)
+	      	(j_nf_ise env (evars_of isevars) funj)
+                (jl_nf_ise env (evars_of isevars) argjl)
 *)
               error_cant_apply_not_functional_loc 
 		(Rawterm.join_loc funloc loc) env
-	      	(j_nf_ise env !isevars resj)
-		(jl_nf_ise env !isevars (List.map snd restjl))
+	      	(j_nf_ise env (evars_of isevars) resj)
+		(jl_nf_ise env (evars_of isevars) (List.map snd restjl))
   in 
   apply_rec env 1 funj argjl
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index a891cdd039..9ac498b38d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -41,10 +41,10 @@ let eval_flexible_term env = function
 
 let evar_apprec env isevars stack c =
   let rec aux s =
-    let (t,stack as s') = Reduction.apprec env !isevars s in
+    let (t,stack as s') = Reduction.apprec env (evars_of isevars) s in
     match kind_of_term t with
-      | IsEvar (n,_ as ev) when Evd.is_defined !isevars n ->
-	  aux (existential_value !isevars ev, stack)
+      | IsEvar (n,_ as ev) when Evd.is_defined (evars_of isevars) n ->
+	  aux (existential_value (evars_of isevars) ev, stack)
       | _ -> (t, list_of_stack stack)
   in aux (c, append_stack (Array.of_list stack) empty_stack)
 
@@ -52,18 +52,18 @@ let evar_apprec env isevars stack c =
  * possibly applied to arguments. *)
 
 let rec evar_conv_x env isevars pbty term1 term2 =
-  let term1 = whd_ise1 !isevars term1 in
-  let term2 = whd_ise1 !isevars term2 in
+  let term1 = whd_ise1 (evars_of isevars) term1 in
+  let term2 = whd_ise1 (evars_of isevars) term2 in
 (*
  if eq_constr term1 term2 then 
     true
   else if (not(has_undefined_isevars isevars term1)) &
     not(has_undefined_isevars isevars term2) 
   then 
-    is_fconv pbty env !isevars term1 term2
+    is_fconv pbty env (evars_of isevars) term1 term2
   else
 *)
-  (is_fconv pbty env !isevars term1 term2) or
+  (is_fconv pbty env (evars_of isevars) term1 term2) or
   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
@@ -74,7 +74,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 (pbty,applist(t1,l1),applist(t2,l2)); true)
+      (add_conv_pb isevars (pbty,applist(t1,l1),applist(t2,l2)); true)
     else 
       evar_eqappr_x env isevars pbty (t1,l1) (t2,l2)
 
@@ -228,7 +228,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	| IsProd (n,c1,c'1), IsProd (_,c2,c'2) when l1=[] & l2=[] -> 
             evar_conv_x env isevars CONV c1 c2
             & 
-	    (let d = nf_ise1 !isevars c1 in
+	    (let d = nf_ise1 (evars_of isevars) c1 in
 	     evar_conv_x (push_rel_assum (n,d) env) isevars pbty c'1 c'2)
 
 	| IsMutInd (sp1,cl1), IsMutInd (sp2,cl2) ->
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index c34e07baca..a8cbe4290f 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -21,6 +21,7 @@ open Reduction
 open Indrec
 open Pretype_errors
 
+
 let rec filter_unique = function
   | [] -> []
   | x::l ->
@@ -48,6 +49,21 @@ let filter_sign p sign x =
 
 let evar_env evd = Global.env_of_context evd.evar_hyps
 
+(* Generator of existential names *)
+let new_evar =
+  let evar_ctr = ref 0 in
+  fun () -> incr evar_ctr; !evar_ctr
+
+let make_evar_instance env =
+  fold_named_context
+    (fun env (id, b, _) l -> (*if b=None then*) mkVar id :: l (*else l*))
+    env []
+
+(* create an untyped existential variable *)
+let new_evar_in_sign env =
+  let ev = new_evar () in
+  mkEvar (ev, Array.of_list (make_evar_instance env))
+
 (*------------------------------------*
  * functional operations on evar sets *
  *------------------------------------*)
@@ -57,7 +73,7 @@ let new_isevar_sign env sigma typ instance =
   let sign = named_context env in
   if not (list_distinct (ids_of_named_context sign)) then 
     error "new_isevar_sign: two vars have the same name";
-  let newev = Evd.new_evar() in
+  let newev = new_evar() in
   let info = { evar_concl = typ; evar_hyps = sign; 
 	       evar_body = Evar_empty; evar_info = None } in
   (Evd.add sigma newev info, mkEvar (newev,Array.of_list instance))
@@ -66,11 +82,6 @@ let new_isevar_sign env sigma typ instance =
    any type has type Type. May cause some trouble, but not so far... *)
 let dummy_sort = mkType dummy_univ
 
-let make_evar_instance env =
-  fold_named_context
-    (fun env (id, b, _) l -> (*if b=None then*) mkVar id :: l (*else l*))
-    env []
-
 (* Declaring any type to be in the sort Type shouldn't be harmful since
    cumulativity now includes Prop and Set in Type. *)
 let new_type_var env sigma =
@@ -134,7 +145,14 @@ let do_restrict_hyps sigma ev args =
  *------------------------------------*)
 
 type evar_constraint = conv_pb * constr * constr
-type 'a evar_defs = 'a Evd.evar_map ref
+type 'a evar_defs =
+    { mutable evars : 'a Evd.evar_map;
+      mutable conv_pbs : evar_constraint list }
+
+let create_evar_defs evd = { evars=evd; conv_pbs=[] }
+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
 
 (* 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
@@ -142,32 +160,33 @@ type 'a evar_defs = 'a Evd.evar_map ref
  * the evar constraints are restored).
  *)
 let ise_try isevars l =
-  let u = !isevars in
+  let u = isevars.evars in
   let rec test = function
-      [] -> isevars := u; false
+      [] -> isevars.evars <- u; false
     | f::l ->
- 	  (try f() with reraise -> isevars := u; raise reraise)
-       or (isevars := u; test 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 sp
+let ise_in_dom isevars sp = Evd.in_dom isevars.evars sp
 
 (* map the given section path to the enamed_declaration *)
-let ise_map isevars sp = Evd.map !isevars sp
+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 = isevars := Evd.define !isevars sp body
+let ise_define isevars sp body =
+  isevars.evars <- Evd.define isevars.evars sp body
 
 (* Does k corresponds to an (un)defined existential ? *)
 let ise_undefined isevars c = match kind_of_term c with
-  | IsEvar (n,_) -> not (Evd.is_defined !isevars n)
+  | IsEvar (n,_) -> not (Evd.is_defined isevars.evars n)
   | _ -> false
 
 let ise_defined isevars c = match kind_of_term c with
-  | IsEvar (n,_) -> Evd.is_defined !isevars n
+  | IsEvar (n,_) -> Evd.is_defined isevars.evars n
   | _ -> false
 
 let need_restriction isevars args = not (array_for_all closed0 args)
@@ -191,11 +210,11 @@ let real_clean isevars sp args rhs =
       | IsEvar (ev,args) ->
 	  let args' = Array.map (subs k) args in
 	  if need_restriction isevars args' then
-	    if Evd.is_defined !isevars ev then 
-	      subs k (existential_value !isevars (ev,args'))
+	    if Evd.is_defined isevars.evars ev then 
+	      subs k (existential_value isevars.evars (ev,args'))
 	    else begin
-	      let (sigma,rc) = do_restrict_hyps !isevars ev args' in
-	      isevars := sigma;
+	      let (sigma,rc) = do_restrict_hyps isevars.evars ev args' in
+	      isevars.evars <- sigma;
 
 	      rc
 	    end
@@ -234,8 +253,8 @@ let new_isevar isevars env typ k =
   let subst,env' = push_rel_context_to_named_context env in
   let typ' = substl subst typ in
   let instance = make_evar_instance_with_rel env in
-  let (sigma',evar) = new_isevar_sign env' !isevars typ' instance in
-  isevars := sigma';
+  let (sigma',evar) = new_isevar_sign env' isevars.evars typ' instance in
+  isevars.evars <- sigma';
   evar
 
 (* [evar_define] solves the problem lhs = rhs when lhs is an uninstantiated
@@ -275,12 +294,12 @@ let evar_define isevars (ev,argsv) rhs =
  *)
 
 let has_undefined_isevars isevars t = 
-  try let _ = whd_ise !isevars t in false
+  try let _ = whd_ise isevars.evars t in false
   with Uninstantiated_evar _ -> true
 
 let head_is_evar isevars = 
   let rec hrec k = match kind_of_term k with
-    | IsEvar (n,_)   -> not (Evd.is_defined !isevars n)
+    | IsEvar (n,_)   -> not (Evd.is_defined isevars.evars n)
     | IsApp (f,_) -> hrec f
     | IsCast (c,_) -> hrec c
     | _ -> false
@@ -332,19 +351,13 @@ let head_evar =
  * ass.
  *)
 
-let conversion_problems = ref ([] : evar_constraint list)
-
-let reset_problems () = conversion_problems := []
-
-let add_conv_pb pb = (conversion_problems := pb::!conversion_problems)
-
 let status_changed lev (pbty,t1,t2) =
   try 
     List.mem (head_evar t1) lev or List.mem (head_evar t2) lev
   with Failure _ ->
     try List.mem (head_evar t2) lev with Failure _ -> false
 
-let get_changed_pb lev =
+let get_changed_pb isevars lev =
   let (pbs,pbs1) = 
     List.fold_left
       (fun (pbs,pbs1) pb ->
@@ -353,9 +366,9 @@ let get_changed_pb lev =
          else 
 	   (pbs,pb::pbs1))
       ([],[])
-      !conversion_problems 
+      isevars.conv_pbs
   in
-  conversion_problems := pbs1;
+  isevars.conv_pbs <- pbs1;
   pbs
 
 (* Solve pbs (?i x1..xn) = (?i y1..yn) which arises often in fixpoint
@@ -365,7 +378,7 @@ let get_changed_pb lev =
 
 let solve_refl conv_algo env isevars ev argsv1 argsv2 =
   if argsv1 = argsv2 then [] else
-  let evd = Evd.map !isevars ev in
+  let evd = Evd.map isevars.evars ev in
   let env = evar_env evd in
   let hyps = evd.evar_hyps in
   let (_,rsign) = 
@@ -379,11 +392,11 @@ let solve_refl conv_algo env isevars ev 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 = Evd.new_evar () in
+  let newev = new_evar () in
   let info = { evar_concl = evd.evar_concl; evar_hyps = nsign;
 	       evar_body = Evar_empty; evar_info = None } in
-  isevars :=
-    Evd.define (Evd.add !isevars newev info) ev (mkEvar (newev,nargs));
+  isevars.evars <-
+    Evd.define (Evd.add isevars.evars newev info) ev (mkEvar (newev,nargs));
   [ev]
 
 
@@ -394,9 +407,10 @@ 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_ise1 !isevars t2 in
+  let t2 = nf_ise1 isevars.evars t2 in
   let lsp = match kind_of_term t2 with
-    | IsEvar (n2,args2 as ev2) when not (Evd.is_defined !isevars n2) ->
+    | IsEvar (n2,args2 as ev2)
+        when not (Evd.is_defined isevars.evars n2) ->
 	if n1 = n2 then
 	  solve_refl conv_algo env isevars n1 args1 args2
 	else
@@ -406,7 +420,7 @@ let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) =
 	    evar_define isevars ev1 t2
     | _ ->
 	evar_define isevars ev1 t2 in
-  let pbs = get_changed_pb lsp in
+  let pbs = get_changed_pb isevars lsp in
   List.for_all (fun (pbty,t1,t2) -> conv_algo env isevars pbty t1 t2) pbs
 
 (* Operations on value/type constraints *)
@@ -448,13 +462,13 @@ let mk_valcon c = Some c
 let split_tycon loc env isevars = function
   | None -> None,None
   | Some c ->
-      let t = whd_betadeltaiota env !isevars c in
+      let t = whd_betadeltaiota env isevars.evars c in
       match kind_of_term t with
         | IsProd (na,dom,rng) -> Some dom, Some rng
 	| _ ->
 	    if ise_undefined isevars t then
-	      let (sigma,dom,rng) = split_evar_to_arrow !isevars t in
-	      isevars := sigma;
+	      let (sigma,dom,rng) = split_evar_to_arrow isevars.evars t in
+	      isevars.evars <- sigma;
 	      Some dom, Some rng
 	    else
 	      error_not_product_loc loc env c
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 53f4cb9e32..3b7fabb3fb 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -19,21 +19,23 @@ open Reduction
 
 (*s This modules provides useful functions for unification modulo evars *)
 
+val new_evar : unit -> evar
+val new_evar_in_sign : env -> constr
+
 val evar_env : 'a evar_info -> env
 
-val dummy_sort : constr
-type evar_constraint = conv_pb * constr * constr
-type 'a evar_defs = 'a evar_map ref
+type 'a evar_defs
+val evars_of : 'a evar_defs -> 'a evar_map
+val create_evar_defs : 'a evar_map -> 'a evar_defs
+val evars_reset_evd : 'a evar_map -> 'a evar_defs -> unit
 
-val reset_problems : unit -> unit
-val add_conv_pb : evar_constraint -> unit
+type evar_constraint = conv_pb * constr * constr
+val add_conv_pb : 'a evar_defs -> evar_constraint -> unit
 
 val ise_try : 'a evar_defs -> (unit -> bool) list -> bool
 val ise_undefined : 'a evar_defs -> constr -> bool
 val has_undefined_isevars : 'a evar_defs -> constr -> bool
 
-val make_evar_instance : env -> constr list
-
 val new_isevar : 'a evar_defs -> env -> constr -> path_kind -> constr
 
 val is_eliminator : constr -> bool
@@ -44,6 +46,8 @@ val solve_simple_eqn :
 
 (* Value/Type constraints *)
 
+val dummy_sort : constr
+
 type type_constraint = constr option
 type val_constraint = constr option
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 0e2974b0bb..c1b7503a37 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -112,6 +112,9 @@ let j_nf_ise sigma {uj_val=v;uj_type=t} =
 
 let jv_nf_ise sigma = Array.map (j_nf_ise sigma)
 
+let tj_nf_ise sigma {utj_val=v;utj_type=t} =
+  {utj_val=type_app (nf_ise1 sigma) v;utj_type=t}
+
 (* Utilisé pour inférer le prédicat des Cases *)
 (* Semble exagérement fort *)
 (* Faudra préférer une unification entre les types de toutes les clauses *)
@@ -125,23 +128,23 @@ let evar_type_fixpoint env isevars lna lar vdefj =
 		  (vdefj.(i)).uj_type
 		  (lift lt lar.(i))) then
           error_ill_typed_rec_body CCI env i lna 
-	    (jv_nf_ise !isevars vdefj) 
-	    (Array.map (type_app (nf_ise1 !isevars)) lar)
+	    (jv_nf_ise (evars_of isevars) vdefj) 
+	    (Array.map (type_app (nf_ise1 (evars_of isevars))) lar)
       done
 
-let let_path = make_path ["Core"] (id_of_string "let") CCI
-
 let wrong_number_of_cases_message loc env isevars (c,ct) expn = 
-  let c = nf_ise1 !isevars c and ct = nf_ise1 !isevars ct in
+  let c = nf_ise1 (evars_of isevars) c
+  and ct = nf_ise1 (evars_of isevars) ct in
   error_number_branches_loc loc CCI env c ct expn
 
 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 c = nf_ise1 !isevars c
-      and lfi = nf_betaiota env !isevars (nf_ise1 !isevars lft.(i)) in
+      let c = nf_ise1 (evars_of isevars) c
+      and lfi = nf_betaiota env (evars_of isevars)
+        (nf_ise1 (evars_of isevars) lft.(i)) in
       error_ill_formed_branch_loc loc CCI env c i lfi 
-	(nf_betaiota env !isevars explft.(i))
+	(nf_betaiota env (evars_of isevars) explft.(i))
   done
 
 (* coerce to tycon if any *)
@@ -151,7 +154,7 @@ let inh_conv_coerce_to_tycon loc env isevars j = function
 
 (*
 let evar_type_case isevars env ct pt lft p c =
-  let (mind,bty,rslty) = type_case_branches env !isevars ct pt p c
+  let (mind,bty,rslty) = type_case_branches env (evars_of isevars) ct pt p c
   in check_branches_message isevars env (c,ct) (bty,lft); (mind,rslty)
 *)
 
@@ -173,7 +176,7 @@ let pretype_id loc env lvar id =
 (* Main pretyping function                                               *)
 
 let pretype_ref isevars env lvar ref = 
-  let c = Declare.constr_of_reference !isevars env ref in
+  let c = Declare.constr_of_reference (evars_of isevars) env ref in
   make_judge c (Retyping.get_type_of env Evd.empty c)
 
 (*
@@ -182,27 +185,27 @@ let pretype_ref _ isevars env lvar ref =
 
 | RConst (sp,ctxt) ->
     let cst = (sp,Array.map pretype ctxt) in
-    make_judge (mkConst cst) (type_of_constant env !isevars cst)
+    make_judge (mkConst cst) (type_of_constant env (evars_of isevars) cst)
 *)
 (* A traiter mais les tables globales nécessaires à cela pour l'instant
 | REVar (sp,ctxt) ->
     let ev = (sp,Array.map pretype ctxt) in
     let body = 
-      if Evd.is_defined !isevars sp then
-	existential_value !isevars ev
+      if Evd.is_defined (evars_of isevars) sp then
+	existential_value (evars_of isevars) ev
       else
 	mkEvar ev
     in
-    let typ = existential_type !isevars ev in
+    let typ = existential_type (evars_of isevars) ev in
     make_judge body typ
 
 | RInd (ind_sp,ctxt) ->
     let ind = (ind_sp,Array.map pretype ctxt) in
-    make_judge (mkMutInd ind) (type_of_inductive env !isevars ind)
+    make_judge (mkMutInd ind) (type_of_inductive env (evars_of isevars) ind)
  
 | RConstruct (cstr_sp,ctxt) ->
     let cstr = (cstr_sp,Array.map pretype ctxt) in
-    let typ = type_of_constructor env !isevars cstr in
+    let typ = type_of_constructor env (evars_of isevars) cstr in
     { uj_val=mkMutConstruct cstr; uj_type=typ }
 *)
 let pretype_sort = function
@@ -212,7 +215,7 @@ let pretype_sort = function
 	uj_type = dummy_sort }
 
 (* [pretype tycon env isevars lvar lmeta cstr] attempts to type [cstr] *)
-(* in environment [env], with existential variables [!isevars] and *)
+(* in environment [env], with existential variables [(evars_of isevars)] and *)
 (* the type constraint tycon *)
 let rec pretype tycon env isevars lvar lmeta = function
 
@@ -229,10 +232,10 @@ let rec pretype tycon env isevars lvar lmeta = function
   | REvar (loc, ev) ->
       (* 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 !isevars ev).evar_hyps in
+      let hyps = (Evd.map (evars_of isevars) ev).evar_hyps in
       let args = instance_from_named_context hyps in
       let c = mkEvar (ev, Array.of_list args) in
-      let j = (Retyping.get_judgment_of env !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
 
   | RMeta (loc,n) ->
@@ -277,11 +280,11 @@ let rec pretype tycon env isevars lvar lmeta = function
 	match fixkind with
 	  | RFix (vn,i as vni) ->
 	      let fix = (vni,(lara,List.rev lfi,Array.map j_val vdefj)) in
-	      check_fix env !isevars fix;
+	      check_fix env (evars_of isevars) fix;
 	      make_judge (mkFix fix) lara.(i)
 	  | RCoFix i -> 
 	      let cofix = (i,(lara,List.rev lfi,Array.map j_val vdefj)) in
-	      check_cofix env !isevars cofix;
+	      check_cofix env (evars_of isevars) cofix;
 	      make_judge (mkCoFix cofix) lara.(i) in
       inh_conv_coerce_to_tycon loc env isevars fixj tycon
 
@@ -296,7 +299,7 @@ let rec pretype tycon env isevars lvar lmeta = function
 	| c::rest ->
 	    let argloc = loc_of_rawconstr c in
 	    let resj = inh_app_fun env isevars resj in
-      	    match kind_of_term (whd_betadeltaiota env !isevars resj.uj_type) with
+      	    match kind_of_term (whd_betadeltaiota env (evars_of isevars) resj.uj_type) with
 	      | IsProd (na,c1,c2) ->
 		  let hj = pretype (mk_tycon c1) env isevars lvar lmeta c in
 		  let newresj =
@@ -311,8 +314,8 @@ let rec pretype tycon env isevars lvar lmeta = function
 		  let hj = pretype empty_tycon env isevars lvar lmeta c in
 		  error_cant_apply_not_functional_loc 
 		    (Rawterm.join_loc floc argloc) env
-	      	    (j_nf_ise env !isevars resj)
-		    [j_nf_ise env !isevars hj]
+	      	    (j_nf_ise env (evars_of isevars) resj)
+		    [j_nf_ise env (evars_of isevars) hj]
 
       in let resj = apply_rec env 1 fj args in
       (*
@@ -336,7 +339,7 @@ let rec pretype tycon env isevars lvar lmeta = function
       let var = (name,j.utj_val) in
       let j' = pretype rng (push_rel_assum var env) isevars lvar lmeta c2 
       in 
-      fst (abs_rel env !isevars name j.utj_val j')
+      fst (abs_rel env (evars_of isevars) name j.utj_val j')
 
   | RProd(loc,name,c1,c2)        ->
       let j = pretype_type empty_valcon env isevars lvar lmeta c1 in
@@ -344,7 +347,7 @@ let rec pretype tycon env isevars lvar lmeta = function
       let env' = push_rel_assum var env in
       let j' = pretype_type empty_valcon env' isevars lvar lmeta c2 in
       let resj =
-	try fst (gen_rel env !isevars name j j')
+	try fst (gen_rel env (evars_of isevars) name j j')
 	with TypeError _ as e -> Stdpp.raise_with_loc loc e in
       inh_conv_coerce_to_tycon loc env isevars resj tycon
 	
@@ -358,14 +361,16 @@ let rec pretype tycon env isevars lvar lmeta = function
   | ROldCase (loc,isrec,po,c,lf) ->
       let cj = pretype empty_tycon env isevars lvar lmeta c in
       let (IndType (indf,realargs) as indt) = 
-	try find_rectype env !isevars cj.uj_type
+	try find_rectype env (evars_of isevars) cj.uj_type
 	with Induc -> error_case_not_inductive CCI env
-	    (nf_ise1 !isevars cj.uj_val) (nf_ise1 !isevars cj.uj_type) in
+	    (nf_ise1 (evars_of isevars) cj.uj_val)
+            (nf_ise1 (evars_of isevars) cj.uj_type) in
       let pj = match po with
 	| Some p -> pretype empty_tycon env isevars lvar lmeta p
 	| None -> 
 	    try match tycon with
-		Some pred -> Retyping.get_judgment_of env !isevars pred
+		Some pred ->
+                  Retyping.get_judgment_of env (evars_of isevars) pred
 	      | None -> error "notype"
 	    with UserError _ -> (* get type information from type of branches*)
 	      let expbr = Cases.branch_scheme env isevars isrec indf in
@@ -377,21 +382,24 @@ let rec pretype tycon env isevars lvar lmeta = function
 		    let expti = expbr.(i) in
 		    let fj =
 		      pretype (mk_tycon expti) env isevars lvar lmeta lf.(i) in
-		    let efjt = nf_ise1 !isevars fj.uj_type in 
+		    let efjt = nf_ise1 (evars_of isevars) fj.uj_type in 
 		    let pred = 
-		      Cases.pred_case_ml_onebranch loc env !isevars isrec indt
+		      Cases.pred_case_ml_onebranch
+                        loc env (evars_of isevars) isrec indt
 			(i,fj.uj_val,efjt) in
 		    if has_undefined_isevars isevars pred then findtype (i+1)
 		    else 
-		      let pty = Retyping.get_type_of env !isevars pred in
+		      let pty =
+                        Retyping.get_type_of env (evars_of isevars) pred in
 		      { uj_val = pred; 
 			uj_type = pty }
 		  with UserError _ -> findtype (i+1) in
 	      findtype 0 in
 
-      let evalPt = nf_ise1 !isevars pj.uj_type in
+      let evalPt = nf_ise1 (evars_of isevars) pj.uj_type in
 
-      let dep = find_case_dep_nparams env !isevars (cj.uj_val,pj.uj_val) indf evalPt in
+      let dep = find_case_dep_nparams env (evars_of isevars)
+        (cj.uj_val,pj.uj_val) indf evalPt in
 
       let (p,pt) =
 	if dep then (pj.uj_val, evalPt) else
@@ -408,10 +416,11 @@ let rec pretype tycon env isevars lvar lmeta = function
 	  let ccl' = mkLambda (Anonymous, ind, ccl) in
 	  (lam_it ccl' sign, prod_it s' sign) in
       let (bty,rsty) =
-	Indrec.type_rec_branches isrec env !isevars indt pt p cj.uj_val in
+	Indrec.type_rec_branches
+          isrec env (evars_of isevars) indt pt p cj.uj_val in
       if Array.length bty <> Array.length lf then
 	wrong_number_of_cases_message loc env isevars 
-	  (cj.uj_val,nf_ise1 !isevars cj.uj_type)
+	  (cj.uj_val,nf_ise1 (evars_of isevars) cj.uj_type)
 	  (Array.length bty)
       else
 	let lfj =
@@ -424,7 +433,7 @@ let rec pretype tycon env isevars lvar lmeta = function
 	let v =
 	  if isrec
 	  then 
-	    transform_rec loc env !isevars(p,cj.uj_val,lfv) (indt,pt)
+	    transform_rec loc env (evars_of isevars)(p,cj.uj_val,lfv) (indt,pt)
 	  else
 	    let mis,_ = dest_ind_family indf in
 	    let ci = make_default_case_info mis in
@@ -441,16 +450,17 @@ let rec pretype tycon env isevars lvar lmeta = function
   | RCast(loc,c,t) ->
       let tj = pretype_type (valcon_of_tycon tycon) env isevars lvar lmeta t in
       let cj = pretype (mk_tycon tj.utj_val) env isevars lvar lmeta c in
+      let cj = {uj_val = mkCast (cj.uj_val,tj.utj_val); uj_type=tj.utj_val} in
       inh_conv_coerce_to_tycon loc env isevars cj tycon
 
-	     (* [pretype_type valcon env isevars lvar lmeta c] coerces [c] into a type *)
+(* [pretype_type valcon env isevars lvar lmeta c] coerces [c] into a type *)
 and pretype_type valcon env isevars lvar lmeta = function
   | RHole loc ->
       if !compter then nbimpl:=!nbimpl+1;
       (match valcon with
 	 | Some v ->
 	     { utj_val = v;
-	       utj_type = Retyping.get_sort_of env !isevars v }
+	       utj_type = Retyping.get_sort_of env (evars_of isevars) v }
 	 | None ->
 	     { utj_val = new_isevar isevars env dummy_sort CCI;
 	       utj_type = Type Univ.dummy_univ })
@@ -460,66 +470,60 @@ and pretype_type valcon env isevars lvar lmeta = function
       match valcon with
 	| None -> tj
 	| Some v ->
-	    if the_conv_x_leq env isevars v tj.utj_val
-	    then
-	      { utj_val = nf_ise1 !isevars tj.utj_val;
-		utj_type = tj.utj_type }
+	    if the_conv_x_leq env isevars v tj.utj_val then tj
 	    else
 	      error_unexpected_type_loc (loc_of_rawconstr c) env tj.utj_val v
 
 
 let unsafe_infer tycon isevars env lvar lmeta constr =
-  reset_problems ();
-  pretype tycon env isevars lvar lmeta constr
+  let j = pretype tycon env isevars lvar lmeta constr in
+  j_nf_ise (evars_of isevars) j
 
 let unsafe_infer_type valcon isevars env lvar lmeta constr =
-  reset_problems ();
-  pretype_type valcon env isevars lvar lmeta constr
+  let tj = pretype_type valcon env isevars lvar lmeta constr in
+  tj_nf_ise (evars_of isevars) tj
 
-(* If fail_evar is false, [process_evars] turns unresolved Evar that
-   were not in initial sigma into Meta's; otherwise it fail on the first
-   unresolved Evar not already in the initial sigma
-   Rem: Does a side-effect on reference metamap *)
+(* If fail_evar is false, [process_evars] builds a meta_map with the
+   unresolved Evar that were not in initial sigma; otherwise it fail
+   on the first unresolved Evar not already in the initial sigma. *)
 (* [fail_evar] says how to process unresolved evars:
  *   true -> raise an error message
  *   false -> convert them into new Metas (casted with their type)
  *)
-let process_evars fail_evar initial_sigma sigma metamap c =
+(* assumes the defined existentials have been replaced in c (should be
+   done in unsafe_infer and unsafe_infer_type) *)
+let check_evars fail_evar initial_sigma sigma c =
+  let metamap = ref [] in
   let rec proc_rec c =
     match kind_of_term c with
-      | IsEvar (ev,args as k) when Evd.in_dom sigma ev ->
-	  if Evd.is_defined sigma ev then
-      	    proc_rec (existential_value sigma k)
-	  else
-	    if Evd.in_dom initial_sigma ev then
-	      c
-	    else
-	      if fail_evar then
-		errorlabstrm "whd_ise"
-		  [< 'sTR"There is an unknown subterm I cannot solve" >]
-	      else
-		let n = new_meta () in
-		metamap := (n, existential_type sigma k) :: !metamap;
-		mkMeta n
-      | _ -> map_constr proc_rec c      
+      | IsEvar (ev,args as k) ->
+          assert (Evd.in_dom sigma ev);
+	  if not (Evd.in_dom initial_sigma ev) then
+	    (if fail_evar then
+	      errorlabstrm "whd_ise"
+		[< 'sTR"There is an unknown subterm I cannot solve" >]
+	    else (* try to avoid duplication *)
+              (if not (List.exists (fun (k',_) -> k=k') !metamap) then
+	        metamap := (k, existential_type sigma k) :: !metamap))
+      | _ -> iter_constr proc_rec c      
   in
-  proc_rec c
- 
+  (proc_rec c; !metamap)
+
 (* TODO: comment faire remonter l'information si le typage a resolu des
        variables du sigma original. il faudrait que la fonction de typage
        retourne aussi le nouveau sigma...
 *)
 
-type meta_map = (int * unsafe_judgment) list
-type var_map = (identifier * unsafe_judgment) list
+(* constr with holes *)
+type open_constr = (existential * types) list * constr
 
 let ise_resolve_casted_gen fail_evar sigma env lvar lmeta typ c =
-  let isevars = ref sigma in
+  let isevars = create_evar_defs sigma in
   let j = unsafe_infer (mk_tycon typ) isevars env lvar lmeta c in
-  let metamap = ref [] in
-  let v = process_evars fail_evar sigma !isevars metamap j.uj_val in
-  let t = type_app (process_evars fail_evar sigma !isevars metamap) j.uj_type in
-  !metamap, {uj_val = v; uj_type = t }
+  let metamap =
+    check_evars fail_evar sigma (evars_of isevars)
+      (mkCast(j.uj_val,j.uj_type)) in
+  (metamap, j)
 
 let ise_resolve_casted sigma env typ c =
   ise_resolve_casted_gen true sigma env [] [] typ c
@@ -529,19 +533,22 @@ 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 lmeta exptyp c =
   let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
-  let isevars = ref sigma in
+  let isevars = create_evar_defs sigma in
   let j = unsafe_infer tycon isevars env lvar lmeta c in
-  let metamap = ref [] in
-  let v = process_evars fail_evar sigma !isevars metamap j.uj_val in
-  let t = type_app (process_evars fail_evar sigma !isevars metamap) j.uj_type in
-  !metamap, {uj_val = v; uj_type = t }
+  let metamap =
+    check_evars fail_evar sigma (evars_of isevars)
+      (mkCast(j.uj_val,j.uj_type)) in
+  (metamap, j)
 
 let ise_infer_type_gen fail_evar sigma env lvar lmeta c =
-  let isevars = ref sigma in
+  let isevars = create_evar_defs sigma in
   let tj = unsafe_infer_type empty_valcon isevars env lvar lmeta c in
-  let metamap = ref [] in
-  let v = process_evars fail_evar sigma !isevars metamap tj.utj_val in
-  !metamap, {utj_val = v; utj_type = tj.utj_type }
+  let metamap =
+    check_evars fail_evar sigma (evars_of isevars) tj.utj_val in
+  (metamap, tj)
+
+type meta_map = (int * unsafe_judgment) list
+type var_map = (identifier * unsafe_judgment) list
 
 let understand_judgment sigma env c =
   snd (ise_infer_gen true sigma env [] [] None c)
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index f0bc559aef..ae6161f502 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -21,6 +21,10 @@ open Evarutil
 type meta_map = (int * unsafe_judgment) list
 type var_map = (identifier * unsafe_judgment) list
 
+(* constr with holes *)
+type open_constr = (existential * types) list * constr
+
+
 (* Generic call to the interpreter from rawconstr to constr, failing
    unresolved holes in the rawterm cannot be instantiated.
 
@@ -41,7 +45,7 @@ val understand_gen :
    these metas. Work as [understand_gen] for the rest. *)
 val understand_gen_tcc :
   'a evar_map -> env -> var_map -> meta_map 
-    -> constr option -> rawconstr -> (int * constr) list * constr
+    -> constr option -> rawconstr -> open_constr
 
 (* Standard call to get a constr from a rawconstr, resolving implicit args *)
 val understand : 'a evar_map -> env -> rawconstr -> constr
@@ -61,12 +65,10 @@ val understand_type_judgment : 'a evar_map -> env -> rawconstr
  * Unused outside, but useful for debugging
  *)
 val pretype : 
-  type_constraint -> env -> 'a evar_defs ->
-    (identifier * unsafe_judgment) list -> (int * unsafe_judgment) list ->
+  type_constraint -> env -> 'a evar_defs -> var_map -> meta_map ->
     rawconstr -> unsafe_judgment
 
 val pretype_type : 
-  val_constraint -> env -> 'a evar_defs ->
-    (identifier * unsafe_judgment) list -> (int * unsafe_judgment) list ->
+  val_constraint -> env -> 'a evar_defs -> var_map -> meta_map ->
     rawconstr -> unsafe_type_judgment
 (*i*)