hiding the meta_map in evar_defs

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

25 files changed, 398 insertions, 405 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 463788a226..9e10c93909 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -63,13 +63,13 @@ 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 =
-  e_new_isevar isevars env loc (new_Type ())
+let mkExistential env ?(src=(dummy_loc,Evd.InternalHole)) isevars =
+  e_new_evar isevars env ~src:src (new_Type ())
 
 let norec_branch_scheme env isevars cstr =
   let rec crec env = function
     | d::rea -> mkProd_or_LetIn d (crec (push_rel d env) rea)
-    | [] -> mkExistential isevars env (dummy_loc, InternalHole) in 
+    | [] -> mkExistential env isevars in 
   crec env (List.rev cstr.cs_args)
 
 let rec_branch_scheme env isevars (sp,j) recargs cstr =
@@ -79,8 +79,7 @@ let rec_branch_scheme env isevars (sp,j) recargs cstr =
 	  let d =
  	    match dest_recarg ra with 
 	      | Mrec k when k=j ->
-		  let t = mkExistential isevars env (dummy_loc, InternalHole)
-		  in
+		  let t = mkExistential env isevars in
 		  mkArrow t
 		    (crec (push_rel (Anonymous,None,t) env)
 		       (List.rev (lift_rel_context 1 (List.rev rea)),reca))
@@ -89,7 +88,7 @@ let rec_branch_scheme env isevars (sp,j) recargs cstr =
 
       | (name,Some b,c as d)::rea, reca -> 
 	  mkLetIn (name,b, c,crec (push_rel d env) (rea,reca))
-      | [],[] -> mkExistential isevars env (dummy_loc, InternalHole)
+      | [],[] -> mkExistential env isevars
       | _ -> anomaly "rec_branch_scheme"
   in 
   crec env (List.rev cstr.cs_args,recargs) 
@@ -154,7 +153,7 @@ let pred_case_ml env sigma isrec (IndType (indf,realargs)) (i,ft) =
     let j = snd ind in (* index of inductive *)
     let nbrec = if isrec then count_rec_arg j recargi else 0 in
     let nb_arg = List.length (recargs.(i)) + nbrec in
-    let pred = Evarutil.refresh_universes (concl_n env sigma nb_arg ft) in
+    let pred = refresh_universes (concl_n env sigma nb_arg ft) in
     if noccur_between 1 nb_arg pred then 
       lift (-nb_arg) pred
     else 
@@ -379,7 +378,7 @@ let push_history_pattern n current cont =
 *)
 type pattern_matching_problem =
     { env      : env;
-      isevars  : evar_defs ref;
+      isevars  : Evd.evar_defs ref;
       pred     : predicate_signature option;
       tomatch  : tomatch_stack;
       history  : pattern_continuation;
@@ -405,15 +404,15 @@ 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 (Evd.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
+    | Some loc -> fun i -> (loc, Evd.TomatchTypeParameter (tyi,i))
+    | None -> fun _ -> (dummy_loc, Evd.InternalHole) in
    let (_,evarl,_) =
     List.fold_right
       (fun (na,ty) (env,evl,n) ->
 	 (push_rel (na,None,ty) env,
-	    (e_new_isevar isevars env (hole_source n) ty)::evl,n+1))
+	    (e_new_evar isevars env ~src:(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 
@@ -432,17 +431,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 (Evd.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 (Evd.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 (Evd.evars_of !isevars) typ)
       with Not_found -> NotInd (None,typ)
 
 let coerce_row typing_fun isevars env cstropt tomatch =
@@ -906,7 +905,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) (evars_of isevars)) p) pv in
+  let pv'= Array.map (fun (n,sign,_,p) -> n,splay_constr (whd_betaiotaevar (push_rels (List.rev sign) env) (Evd.evars_of 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
@@ -930,7 +929,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 (Evd.evars_of !isevars))) typs
     in
     let eqns = array_map2 prepare_unif_pb typs cstrs in
     (* First strategy: no dependencies at all *)
@@ -941,7 +940,7 @@ let infer_predicate loc env isevars typs cstrs indf =
 	(* Heuristic to avoid comparison between non-variables algebric univs*)
 	new_Type ()
       else
-	mkExistential isevars env (loc, CasesType)
+	mkExistential env ~src:(loc, Evd.CasesType) isevars
     in
     if array_for_all (fun (_,_,typ) -> e_cumul env isevars typ mtyp) eqns
     then
@@ -1128,7 +1127,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 (Evd.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
@@ -1368,7 +1367,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 (Evd.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 *)
@@ -1586,13 +1585,13 @@ 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 (Evd.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 *)
     (* We turn all subterms possibly dependent into an evar with maximum ctxt*)
     if isEvar c or List.exists (eq_constr c) allargs then
-      mkExistential isevars env (loc, CasesType)
+      mkExistential env ~src:(loc, Evd.CasesType) isevars
     else
       map_constr_with_full_binders push_rel build_skeleton env c in
   build_skeleton env (lift n c)
@@ -1700,21 +1699,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 = Evd.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 _)) ->
-        isevars := evars_reset_evd isevars_copy !isevars;
+        isevars := Evd.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 _)) ->
-        isevars := evars_reset_evd isevars_copy !isevars;
+        isevars := Evd.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 *)
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 5b4ed65714..450c87a1f0 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -48,7 +48,6 @@ type clausenv = {
   namenv   : identifier Metamap.t }
 
 let cl_env ce = ce.templenv
-let cl_metas ce = metas_of ce.env
 let cl_sigma ce = evars_of ce.env
 
 let subst_clenv sub clenv = 
@@ -57,14 +56,14 @@ let subst_clenv sub clenv =
     namenv = clenv.namenv;
     env = reset_evd
       (evars_of clenv.env,
-       Metamap.map (map_clb (subst_mps sub)) (cl_metas clenv))
+       Metamap.map (map_clb (subst_mps sub)) (metas_of clenv.env))
       clenv.env;
     templenv = clenv.templenv }
 
-let clenv_nf_meta clenv c = nf_meta (cl_metas clenv) c
-let clenv_meta_type clenv mv = meta_type (cl_metas clenv) mv
-let clenv_value clenv = meta_instance (cl_metas clenv) clenv.templval
-let clenv_type clenv = meta_instance (cl_metas clenv) clenv.templtyp
+let clenv_nf_meta clenv c = nf_meta clenv.env c
+let clenv_meta_type clenv mv = meta_type clenv.env mv
+let clenv_value clenv = meta_instance clenv.env clenv.templval
+let clenv_type clenv = meta_instance clenv.env clenv.templtyp
 
 
 let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
@@ -75,12 +74,12 @@ let clenv_get_type_of ce c =
       (function
 	 | (n,Clval(_,typ)) -> (n,typ.rebus)
          | (n,Cltyp typ)    -> (n,typ.rebus))
-      (metamap_to_list (cl_metas ce)) in
+      (metamap_to_list (metas_of ce.env)) in
   Retyping.get_type_of_with_meta (cl_env ce) (cl_sigma ce) metamap c
 
 
 
-let clenv_environments bound c =
+let clenv_environments evd bound c =
   let rec clrec (ne,e,metas) n c =
     match n, kind_of_term c with
       | (Some 0, _) -> (ne, e, List.rev metas, c)
@@ -109,14 +108,15 @@ let clenv_environments bound c =
 	  clrec (ne,e,metas) (option_app ((+) (-1)) n) (subst1 b c)
       | (n, _) -> (ne, e, List.rev metas, c)
   in 
-  clrec (Metamap.empty,Metamap.empty,[]) bound c
+  clrec (Metamap.empty,evd,[]) bound c
 
 let mk_clenv_from_n gls n (c,cty) =
-  let (namenv,env,args,concl) = clenv_environments n cty in
+  let evd = create_evar_defs gls.sigma in
+  let (namenv,env,args,concl) = clenv_environments evd n cty in
   { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args));
     templtyp = mk_freelisted concl;
     namenv = namenv;
-    env = mk_evar_defs (gls.sigma,env);
+    env = env;
     templenv = Global.env_of_context gls.it.evar_hyps }
 
 let mk_clenv_from gls = mk_clenv_from_n gls None
@@ -138,7 +138,7 @@ let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)
 let mentions clenv mv0 = 
   let rec menrec mv1 =
     try
-     (match Metamap.find mv1 (cl_metas clenv) with
+     (match Metamap.find mv1 (metas_of clenv.env) with
 	 | Clval (b,_) -> 
 	     Metaset.mem mv0 b.freemetas || meta_exists menrec b.freemetas
 	 | Cltyp _ -> false)
@@ -147,7 +147,7 @@ let mentions clenv mv0 =
   in 
   menrec
 
-let clenv_defined clenv mv = meta_defined (cl_metas clenv) mv
+let clenv_defined clenv mv = meta_defined clenv.env mv
 
 (* TODO: replace by clenv_unify (mkMeta mv) rhs ? *)		      
 let clenv_assign mv rhs clenv =
@@ -155,7 +155,7 @@ let clenv_assign mv rhs clenv =
   if meta_exists (mentions clenv mv) rhs_fls.freemetas then
     error "clenv__assign: circularity in unification";
   try
-    (match Metamap.find mv (cl_metas clenv) with
+    (match Metamap.find mv (metas_of clenv.env) with
        | Clval (fls,ty) ->
 	   if not (eq_constr fls.rebus rhs) then
 	     try 
@@ -167,12 +167,7 @@ let clenv_assign mv rhs clenv =
 	       anomaly "clenv_assign: non dependent metavar already assigned"
 	   else
 	     clenv
-       | Cltyp bty -> 
-	   { clenv with
-	     env = reset_evd
-               (cl_sigma clenv,
-                Metamap.add mv (Clval (rhs_fls,bty)) (cl_metas clenv))
-               clenv.env })
+       | Cltyp _ -> {clenv with env = meta_assign mv rhs_fls.rebus clenv.env})
   with Not_found -> 
     error "clenv_assign"
 
@@ -203,12 +198,12 @@ let collect_metas c =
  * returns a list of the metavars which appear in the type of
  * the metavar mv.  The list is unordered. *)
 
-let clenv_metavars clenv mv = (meta_ftype (cl_metas clenv) mv).freemetas
+let clenv_metavars clenv mv = (meta_ftype clenv mv).freemetas
 
 let dependent_metas clenv mvs conclmetas =
   List.fold_right
     (fun mv deps ->
-       Metaset.union deps (clenv_metavars clenv mv))
+       Metaset.union deps (clenv_metavars clenv.env mv))
     mvs conclmetas
 
 let clenv_dependent hyps_only clenv =
@@ -240,12 +235,9 @@ let clenv_pose_dependent_evars clenv =
   let dep_mvs = clenv_dependent false clenv in
   List.fold_left
     (fun clenv mv ->
-       let evar = Evarutil.new_evar_in_sign (cl_env clenv) in
-       let (evar_n,_) = destEvar evar in
-       let tY = clenv_meta_type clenv mv in
-       let clenv' =
-         clenv_wtactic (w_Declare (cl_env clenv) evar_n tY) clenv in
-       clenv_assign mv evar clenv')
+      let ty = clenv_meta_type clenv mv in
+      let (evd,evar) = new_evar clenv.env (cl_env clenv) ty in
+      clenv_assign mv evar {clenv with env=evd})
     clenv
     dep_mvs
 
@@ -286,11 +278,7 @@ let clenv_fchain mv clenv nextclenv =
 			  end else 
 			    Metamap.add mv id ne)
           clenv.namenv (metamap_to_list nextclenv.namenv);
-      env = reset_evd
-        (cl_sigma nextclenv,
-         List.fold_left (fun m (n,v) -> Metamap.add n v m) 
-	       (cl_metas clenv) (metamap_to_list (cl_metas nextclenv)))
-        nextclenv.env;
+      env = meta_merge clenv.env nextclenv.env;
       templenv = nextclenv.templenv } 
   in
   (* unify the type of the template of [nextclenv] with the type of [mv] *)
@@ -474,4 +462,4 @@ let pr_clenv clenv =
   in
   (str"TEMPL: " ++ print_constr clenv.templval.rebus ++
      str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++
-     (prlist pr_meta_binding (metamap_to_list (cl_metas clenv))))
+     (prlist pr_meta_binding (metamap_to_list (metas_of clenv.env))))
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index 30bc96338d..cb53feb908 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -67,8 +67,7 @@ val clenv_fchain : metavariable -> clausenv -> clausenv -> clausenv
 
 (* Unifies two terms in a clenv. The boolean is allow_K (see Unification) *)
 val clenv_unify : 
-  bool -> Reductionops.conv_pb -> constr -> constr ->
-  clausenv -> clausenv
+  bool -> conv_pb -> constr -> constr -> clausenv -> clausenv
 
 (* unifies the concl of the goal with the type of the clenv *)
 val clenv_unique_resolver :
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 347bc7b8e5..51fea11a24 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -19,6 +19,7 @@ open Recordops
 open Evarutil
 open Evarconv
 open Retyping
+open Evd
 
 (* Typing operations dealing with coercions *)
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 086bf61ba5..26b646bdd8 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -23,6 +23,7 @@ open Nameops
 open Termops
 open Libnames
 open Nametab
+open Evd
 
 (****************************************************************************)
 (* Tools for printing of Cases                                              *)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 6454e0e84c..2ed26c92c5 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -19,6 +19,7 @@ open Classops
 open Recordops 
 open Evarutil
 open Libnames
+open Evd
 
 type flex_kind_of_term =
   | Rigid of constr 
@@ -175,13 +176,13 @@ 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  *)
   if
-    (not (has_undefined_isevars isevars term1) &
-    not (has_undefined_isevars isevars term2) &
+    (not (has_undefined_evars isevars term1) &
+    not (has_undefined_evars isevars term2) &
     is_fconv pbty env (evars_of isevars) term1 term2) then
       (isevars,true)
-  else if ise_undefined isevars term1 then
+  else if is_undefined_evar isevars term1 then
     solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term1,term2)
-  else if ise_undefined isevars term2 then
+  else if is_undefined_evar isevars term2 then
     solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term2,term1)
   else 
     let (t1,l1) = apprec_nohdbeta env isevars term1 in
@@ -438,8 +439,8 @@ and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) =
   let (isevars',ks) =
     List.fold_left
       (fun (i,ks) b ->
-	 let dloc = (dummy_loc,Rawterm.InternalHole) in
-         let (i',ev) = new_isevar i env dloc (substl ks b) in
+	 let dloc = (dummy_loc,InternalHole) in
+         let (i',ev) = new_evar i env ~src:dloc (substl ks b) in
 	 (i', ev :: ks))
       (isevars,[]) bs
   in
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 5deccaa8b1..41b5e05fa1 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -13,7 +13,7 @@ open Term
 open Sign
 open Environ
 open Reductionops
-open Evarutil
+open Evd
 (*i*)
 
 (* returns exception Reduction.NotConvertible if not unifiable *)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index cb4efd2e12..276c455fe1 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -120,7 +120,8 @@ let exist_to_meta sigma (emap, c) =
 (*************************************)
 (* Metas *)
 
-let meta_val_of env mv = 
+let meta_val_of evd mv = 
+  let env = metas_of evd in
   let rec valrec mv =
     try
       (match Metamap.find mv env with
@@ -152,10 +153,8 @@ let meta_type env mv =
 (* Creating new evars *)
 (**********************)
 
-let evar_env evd = Global.env_of_context evd.evar_hyps
-
 (* Generator of existential names *)
-let new_evar =
+let new_untyped_evar =
   let evar_ctr = ref 0 in
   fun () -> incr evar_ctr; existential_of_int !evar_ctr
 
@@ -165,8 +164,8 @@ let make_evar_instance env =
     env ~init:[]
 
 (* create an untyped existential variable *)
-let new_evar_in_sign env =
-  let ev = new_evar () in
+let new_untyped_evar_in_sign env =
+  let ev = new_untyped_evar () in
   mkEvar (ev, Array.of_list (make_evar_instance env))
 
 (*------------------------------------*
@@ -174,20 +173,66 @@ let new_evar_in_sign env =
  *------------------------------------*)
 
 (* All ids of sign must be distincts! *)
-let new_isevar_sign env sigma typ instance =
-  let sign = named_context env in
+let new_evar_instance sign evd typ ?(src=(dummy_loc,InternalHole)) instance =
+  assert (List.length instance = named_context_length sign); 
   if not (list_distinct (ids_of_named_context sign)) then 
-    error "new_isevar_sign: two vars have the same name";
-  let newev = new_evar() in
-  let info = { evar_concl = typ; evar_hyps = sign; 
-	       evar_body = Evar_empty } in
-  (Evd.add sigma newev info, mkEvar (newev,Array.of_list instance))
+    error "new_evar_instance: two vars have the same name";
+  let newev = new_untyped_evar() in
+  (evar_declare sign newev typ ~src:src evd,
+   mkEvar (newev,Array.of_list instance))
+
+let make_evar_instance_with_rel env =
+  let n = rel_context_length (rel_context env) in
+  let vars = 
+    fold_named_context
+      (fun env (id,b,_) l -> (* if b=None then *) mkVar id :: l (*else l*))
+      env ~init:[] in
+  snd (fold_rel_context
+	 (fun env (_,b,_) (i,l) -> 
+	    (i-1, (*if b=None then *) mkRel i :: l (*else l*)))
+	 env ~init:(n,vars))
+
+let make_subst env args =
+  snd (fold_named_context
+    (fun env (id,b,c) (args,l as g) ->
+       match b, args with
+	 | (* None *) _ , a::rest -> (rest, (id,a)::l)
+(*	 | Some _, _ -> g*)
+	 | _ -> anomaly "Instance does not match its signature")
+    env ~init:(List.rev args,[]))
+
+(* [new_isevar] declares a new existential in an env env with type typ *)
+(* Converting the env into the sign of the evar to define *)
+
+let push_rel_context_to_named_context env =
+  let sign0 = named_context env in
+  let (subst,_,sign) =
+  Sign.fold_rel_context
+    (fun (na,c,t) (subst,avoid,sign) ->
+       let na = if na = Anonymous then Name(id_of_string"_") else na in
+       let id = next_name_away na avoid in
+       ((mkVar id)::subst,
+        id::avoid,
+	add_named_decl (id,option_app (substl subst) c,
+                        type_app (substl subst) t)
+	  sign))
+    (rel_context env) ~init:([],ids_of_named_context sign0,sign0)
+  in (subst, sign)
+
+let new_evar evd env ?(src=(dummy_loc,InternalHole)) typ =
+  let subst,sign = push_rel_context_to_named_context env in
+  let typ' = substl subst typ in
+  let instance = make_evar_instance_with_rel env in
+  new_evar_instance sign evd typ' ~src:src instance
+
+(* The same using side-effect *)
+let e_new_evar evd env ?(src=(dummy_loc,InternalHole)) ty =
+  let (evd',ev) = new_evar !evd env ~src:src ty in
+  evd := evd';
+  ev
 
 (* We don't try to guess in which sort the type should be defined, since
    any type has type Type. May cause some trouble, but not so far... *)
-let new_Type () = mkType (new_univ ())
-
-let new_Type_sort () = Type (new_univ ())
 
 let judge_of_new_Type () = Typeops.judge_of_type (new_univ ())
 (*
@@ -200,40 +245,7 @@ let judge_of_new_Type () =
     uj_type = mkSort (Type dummy_univ) }
 *)
 
-(* This refreshes universes in types; works only for inferred types (i.e. for
-   types of the form (x1:A1)...(xn:An)B with B a sort or an atom in
-   head normal form) *)
-let refresh_universes t =
-  let modified = ref false in
-  let rec refresh t = match kind_of_term t with
-    | Sort (Type _) -> modified := true; new_Type ()
-    | Prod (na,u,v) -> mkProd (na,u,refresh v)
-    | _ -> t in
-  let t' = refresh t in
-  if !modified then t' else t
 
-(* 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 =
-  let instance = make_evar_instance env in
-  new_isevar_sign env sigma (new_Type ()) instance
-
-let split_evar_to_arrow sigma (ev,args) =
-  let evd = Evd.map sigma ev in
-  let evenv = evar_env evd in
-  let (sigma1,dom) = new_type_var evenv sigma in
-  let hyps = evd.evar_hyps in
-  let nvar = next_ident_away (id_of_string "x") (ids_of_named_context hyps) in
-  let newenv = push_named (nvar, None, dom) evenv in
-  let (sigma2,rng) = new_type_var newenv sigma1 in
-  let x = named_hd newenv dom Anonymous in
-  let prod = mkProd (x, dom, subst_var nvar rng) in
-  let sigma3 = Evd.define sigma2 ev prod in
-  let evdom = fst (destEvar dom), args in
-  let evrng =
-    fst (destEvar rng), array_cons (mkRel 1) (Array.map (lift 1) args) in
-  let prod' = mkProd (x, mkEvar evdom, mkEvar evrng) in
-  (sigma3,prod', evdom, evrng)
 
 (* Redefines an evar with a smaller context (i.e. it may depend on less
  * variables) such that c becomes closed.
@@ -243,11 +255,11 @@ let split_evar_to_arrow sigma (ev,args) =
  * What we do is that ?2 is defined by a new evar ?4 whose context will be
  * a prefix of ?2's env, included in ?1's env. *)
 
-let do_restrict_hyps sigma ev args =
+let do_restrict_hyps evd ev args =
   let args = Array.to_list args in
-  let evd = Evd.map sigma ev in
-  let env = evar_env evd in
-  let hyps = evd.evar_hyps in
+  let evi = Evd.map (evars_of !evd) ev in
+  let env = evar_env evi in
+  let hyps = evi.evar_hyps in
   let (_,(rsign,ncargs)) =
     List.fold_left 
       (fun (sign,(rs,na)) a ->
@@ -261,10 +273,11 @@ let do_restrict_hyps sigma ev args =
   let sign' = List.rev rsign in
   let env' = reset_with_named_context sign' env in
   let instance = make_evar_instance env' in
-  let (sigma',nc) = new_isevar_sign env' sigma evd.evar_concl instance in
-  let nc = refresh_universes nc in (* needed only if nc is an inferred type *)
-  let sigma'' = Evd.define sigma' ev nc in
-  (sigma'', nc)
+  let (evd',nc) =
+    new_evar_instance sign' !evd evi.evar_concl
+      ~src:(evar_source ev !evd) instance in
+  evd := Evd.evar_define ev nc evd';
+  nc
 
 
 
@@ -273,45 +286,6 @@ let do_restrict_hyps sigma ev args =
  * operations on the evar constraints *
  *------------------------------------*)
 
-type maps = evar_map * meta_map
-type evar_constraint = conv_pb * constr * constr
-type evar_defs =
-    { evars : Evd.evar_map;
-      conv_pbs : evar_constraint list;
-      history : (existential_key * (loc * Rawterm.hole_kind)) list;
-      metas : Evd.meta_map }
-
-let mk_evar_defs (sigma,mmap) =
-  { evars=sigma; conv_pbs=[]; history=[]; metas=mmap }
-let create_evar_defs sigma =
-  mk_evar_defs (sigma,Metamap.empty)
-let evars_of d = d.evars
-let metas_of d = d.metas
-let evars_reset_evd evd d = {d with evars = evd}
-let reset_evd (sigma,mmap) d = {d with evars = sigma; metas=mmap}
-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)
-
-(* say if the section path sp corresponds to an existential *)
-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.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 with evars = Evd.define isevars.evars sp body}
-
-let is_defined_evar isevars (n,_) = Evd.is_defined isevars.evars n
-
-(* Does k corresponds to an (un)defined existential ? *)
-let ise_undefined isevars c = match kind_of_term c with
-  | Evar ev -> not (is_defined_evar isevars ev)
-  | _ -> false
-
 let need_restriction isevars args = not (array_for_all closed0 args)
     
 (* The list of non-instantiated existential declarations *)
@@ -343,17 +317,9 @@ let real_clean env isevars ev args rhs =
       | Evar (ev,args) ->
 	  let args' = Array.map (subs k) args in
 	  if need_restriction !evd args' then
-            if Evd.is_defined !evd.evars ev then 
-	      subs k (existential_value !evd.evars (ev,args'))
-	    else begin
-	      let (sigma,rc) = do_restrict_hyps !evd.evars ev args' in
-              evd :=
-	      {!evd with
-               evars = sigma;
-               history = 
-                (fst (destEvar rc),evar_source ev !evd):: !evd.history};
-	      rc
-	    end
+            if Evd.is_defined_evar !evd (ev,args) then 
+	      subs k (existential_value (evars_of !evd) (ev,args'))
+	    else do_restrict_hyps evd ev args'
 	  else
 	    mkEvar (ev,args')
       | Var _ -> (try List.assoc t subst with Not_found -> t)
@@ -361,63 +327,9 @@ let real_clean env isevars ev args rhs =
   in
   let body = subs 0 rhs in
   if not (closed0 body)
-  then error_not_clean env !evd.evars ev body (evar_source ev !evd);
+  then error_not_clean env (evars_of !evd) ev body (evar_source ev !evd);
   (!evd,body)
 
-let make_evar_instance_with_rel env =
-  let n = rel_context_length (rel_context env) in
-  let vars = 
-    fold_named_context
-      (fun env (id,b,_) l -> (* if b=None then *) mkVar id :: l (*else l*))
-      env ~init:[] in
-  snd (fold_rel_context
-	 (fun env (_,b,_) (i,l) -> 
-	    (i-1, (*if b=None then *) mkRel i :: l (*else l*)))
-	 env ~init:(n,vars))
-
-let make_subst env args =
-  snd (fold_named_context
-    (fun env (id,b,c) (args,l as g) ->
-       match b, args with
-	 | (* None *) _ , a::rest -> (rest, (id,a)::l)
-(*	 | Some _, _ -> g*)
-	 | _ -> anomaly "Instance does not match its signature")
-    env ~init:(List.rev args,[]))
-
-(* [new_isevar] declares a new existential in an env env with type typ *)
-(* Converting the env into the sign of the evar to define *)
-
-let push_rel_context_to_named_context env =
-  let sign0 = named_context env in
-  let (subst,_,sign) =
-  Sign.fold_rel_context
-    (fun (na,c,t) (subst,avoid,sign) ->
-       let na = if na = Anonymous then Name(id_of_string"_") else na in
-       let id = next_name_away na avoid in
-       ((mkVar id)::subst,
-        id::avoid,
-	add_named_decl (id,option_app (substl subst) c,
-                        type_app (substl subst) t)
-	  sign))
-    (rel_context env) ~init:([],ids_of_named_context sign0,sign0)
-  in (subst, reset_with_named_context sign env)
-
-let new_isevar isevars env src typ =
-  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.evars typ' instance in
-  {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
@@ -440,24 +352,24 @@ 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 evi = ise_map isevars ev in
+  let evi = Evd.map (evars_of isevars) ev in
   (* the bindings to invert *)
   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
+  let isevars'' = Evd.evar_define ev body isevars' in
   isevars'',[ev]
 
 (*-------------------*)
 (* Auxiliary functions for the conversion algorithms modulo evars
  *)
 
-let has_undefined_isevars isevars t = 
-  try let _ = local_strong (whd_ise isevars.evars) t in false
+let has_undefined_evars isevars t = 
+  try let _ = local_strong (whd_ise (evars_of isevars)) t in false
   with Uninstantiated_evar _ -> true
 
 let head_is_evar isevars = 
   let rec hrec k = match kind_of_term k with
-    | Evar (n,_)   -> not (Evd.is_defined isevars.evars n)
+    | Evar n   -> not (Evd.is_defined_evar isevars n)
     | App (f,_) -> hrec f
     | Cast (c,_) -> hrec c
     | _ -> false
@@ -515,20 +427,6 @@ let status_changed lev (pbty,t1,t2) =
   with Failure _ ->
     try List.mem (head_evar t2) lev with Failure _ -> false
 
-let get_changed_pb isevars lev =
-  let (pbs,pbs1) = 
-    List.fold_left
-      (fun (pbs,pbs1) pb ->
-    	 if status_changed lev pb then 
-	   (pb::pbs,pbs1)
-         else 
-	   (pbs,pb::pbs1))
-      ([],[])
-      isevars.conv_pbs
-  in
-  {isevars with conv_pbs = pbs1},
-  pbs
-
 (* Solve pbs (?i x1..xn) = (?i y1..yn) which arises often in fixpoint
  * definitions. We try to unify the xi with the yi pairwise. The pairs
  * that don't unify are discarded (i.e. ?i is redefined so that it does not
@@ -536,7 +434,7 @@ let get_changed_pb isevars lev =
 
 let solve_refl conv_algo env isevars ev argsv1 argsv2 =
   if argsv1 = argsv2 then (isevars,[]) else
-  let evd = Evd.map isevars.evars ev in
+  let evd = Evd.map (evars_of isevars) ev in
   let hyps = evd.evar_hyps in
   let (isevars',_,rsign) = 
     array_fold_left2
@@ -549,15 +447,11 @@ let solve_refl conv_algo env isevars ev argsv1 argsv2 =
       (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 with
-   evars =
-    Evd.define (Evd.add isevars.evars newev info) ev (mkEvar (newev,nargs));
-   history = (newev,evar_source ev isevars)::isevars.history},
-  [ev]
+  let (evd',newev) =
+    new_evar isevars (reset_with_named_context nsign env)
+      ~src:(evar_source ev isevars) evd.evar_concl in
+  let evd'' = Evd.evar_define ev newev evd' in
+  evd'', [ev]
 
 
 (* Tries to solve problem t1 = t2.
@@ -567,7 +461,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 t2 = nf_evar (evars_of isevars) t2 in
   let (isevars,lsp) = match kind_of_term t2 with
     | Evar (n2,args2 as ev2) ->
 	if n1 = n2 then
@@ -579,7 +473,7 @@ 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 (isevars,pbs) = get_changed_pb isevars lsp in
+  let (isevars,pbs) = get_conv_pbs isevars (status_changed 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)
@@ -618,23 +512,29 @@ let mk_valcon c = Some c
 
 (* Refining an evar to a product or a sort *)
 
-let refine_evar_as_arrow isevars ev =
-  let (sigma,prod,evdom,evrng) = split_evar_to_arrow isevars.evars ev in
-  let hst = evar_source (fst ev) isevars in
-  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 (isevars',prod,_,_) = refine_evar_as_arrow isevars ev in
-  isevars',prod
+(* Declaring any type to be in the sort Type shouldn't be harmful since
+   cumulativity now includes Prop and Set in Type...
+   It is, but that's not too bad *)
+let define_evar_as_arrow evd (ev,args) =
+  let evi = Evd.map (evars_of evd) ev in
+  let evenv = evar_env evi in
+  let (evd1,dom) = new_evar evd evenv (new_Type()) in
+  let nvar =
+    next_ident_away (id_of_string "x") (ids_of_named_context evi.evar_hyps) in
+  let newenv = push_named (nvar, None, dom) evenv in
+  let (evd2,rng) =
+    new_evar evd1 newenv ~src:(evar_source ev evd1) (new_Type()) in
+  let prod = mkProd (Name nvar, dom, subst_var nvar rng) in
+  let evd3 = Evd.evar_define ev prod evd2 in
+  let evdom = fst (destEvar dom), args in
+  let evrng =
+    fst (destEvar rng), array_cons (mkRel 1) (Array.map (lift 1) args) in
+  let prod' = mkProd (Name nvar, mkEvar evdom, mkEvar evrng) in
+  (evd3,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
+  Evd.evar_define ev s isevars, destSort s
 
 
 (* Propagation of constraints through application and abstraction:
@@ -649,9 +549,10 @@ let split_tycon loc env isevars = function
       let t = whd_betadeltaiota env sigma c in
       match kind_of_term t with
         | Prod (na,dom,rng) -> isevars, (na, Some dom, Some rng)
-	| Evar (n,_ as ev) when not (Evd.is_defined isevars.evars n) ->
-	    let (isevars',_,evdom,evrng) = refine_evar_as_arrow isevars ev in
-	    isevars',(Anonymous, Some (mkEvar evdom), Some (mkEvar evrng))
+	| Evar ev when not (Evd.is_defined_evar isevars ev) ->
+	    let (isevars',prod) = define_evar_as_arrow isevars ev in
+            let (_,dom,rng) = destProd prod in
+	    isevars',(Anonymous, Some dom, Some rng)
 	| _ -> 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 6d264b718b..711e107079 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -46,53 +46,43 @@ val whd_castappevar :  evar_map -> constr -> constr
 (* [new_meta] is a generator of unique meta variables *)
 val new_meta : unit -> metavariable
 val mk_new_meta : unit -> constr
-val nf_meta       : meta_map -> constr -> constr
-val meta_type     : meta_map -> metavariable -> types
-val meta_instance : meta_map -> constr freelisted -> constr
+val nf_meta       : evar_defs -> constr -> constr
+val meta_type     : evar_defs -> metavariable -> types
+val meta_instance : evar_defs -> constr freelisted -> constr
 
 (* [exist_to_meta] generates new metavariables for each existential
    and performs the replacement in the given constr *)
 val exist_to_meta : evar_map -> open_constr -> (Termops.metamap * constr)
 
-(* Creating new existential variables *)
-val new_evar : unit -> evar
-val new_evar_in_sign : env -> constr
-
-val evar_env :  evar_info -> env
 
 (***********************************************************)
 
-type maps = evar_map * meta_map
-type evar_defs
-val evars_of : evar_defs -> evar_map
-val metas_of : evar_defs -> meta_map
-
-val non_instantiated : evar_map -> (evar * evar_info) list
-
-val mk_evar_defs :  maps -> evar_defs
-(* the same with empty meta map: *)
-val create_evar_defs :  evar_map -> evar_defs
-val evars_reset_evd :  evar_map ->  evar_defs -> evar_defs
-val reset_evd :  maps ->  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_constraint -> evar_defs -> evar_defs
-
-val is_defined_evar :  evar_defs -> existential -> bool
-val ise_undefined :  evar_defs -> constr -> bool
-val has_undefined_isevars :  evar_defs -> constr -> bool
-
-val new_isevar_sign :
- Environ.env -> Evd.evar_map -> Term.constr -> Term.constr list ->
-  Evd.evar_map * Term.constr
+(* Creating a fresh evar given their type and context *)
+val new_evar :
+  evar_defs -> env -> ?src:loc * hole_kind -> types -> evar_defs * constr
+(* the same with side-effects *)
+val e_new_evar :
+  evar_defs ref -> env -> ?src:loc * hole_kind -> types -> constr
+
+(* Create a fresh evar in a context different from its definition context:
+   [new_evar_instance sign evd ty inst] creates a new evar of context
+   [sign] and type [ty], [inst] is a mapping of the evar context to
+   the context where the evar should occur. This means that the terms 
+   of [inst] are typed in the occurrence context and their type (seen
+   as a telescope) is [sign] *)
+val new_evar_instance :
+ named_context -> evar_defs -> types -> ?src:loc * hole_kind -> constr list ->
+ evar_defs * constr
+
+(* Builds the instance in the case where the occurrence context is the
+   same as the evar context *)
+val make_evar_instance : env -> constr list
 
-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 non_instantiated : evar_map -> (evar * evar_info) list
 
+val has_undefined_evars :  evar_defs -> constr -> bool
 val is_eliminator : constr -> bool
 val head_is_embedded_evar :  evar_defs -> constr -> bool
 val solve_simple_eqn :
@@ -106,10 +96,7 @@ val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts
 (***********************************************************)
 (* Value/Type constraints *)
 
-val new_Type_sort : unit -> sorts
-val new_Type : unit -> constr
 val judge_of_new_Type : unit -> unsafe_judgment
-val refresh_universes : types -> types
 
 type type_constraint = constr option
 type val_constraint = constr option
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index d7468eded5..c91d9ae7da 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -13,6 +13,7 @@ open Names
 open Term
 open Sign
 open Environ
+open Libnames
 
 (* The type of mappings for existential variables *)
 
@@ -60,6 +61,7 @@ let is_defined sigma ev =
   not (info.evar_body = Evar_empty)
 
 let evar_body ev = ev.evar_body
+let evar_env evd = Global.env_of_context evd.evar_hyps
 
 let string_of_existential ev = "?" ^ string_of_int ev
 
@@ -184,25 +186,103 @@ let metamap_to_list m =
 let metamap_inv m b =
   Metamap.fold (fun n v l -> if v = b then n::l else l) m []
  
+(*************************)
+(* Unification state *)
+
+type hole_kind =
+  | ImplicitArg of global_reference * (int * identifier option)
+  | BinderType of name
+  | QuestionMark
+  | CasesType
+  | InternalHole
+  | TomatchTypeParameter of inductive * int
+
+type conv_pb = 
+  | CONV 
+  | CUMUL
+
 type meta_map = clbinding Metamap.t
- 
-let meta_defined env mv =
-  match Metamap.find mv env with
+type evar_constraint = conv_pb * constr * constr
+type evar_defs =
+    { evars : evar_map;
+      conv_pbs : evar_constraint list;
+      history : (existential_key * (loc * hole_kind)) list;
+      metas : meta_map }
+
+let mk_evar_defs (sigma,mmap) =
+  { evars=sigma; conv_pbs=[]; history=[]; metas=mmap }
+let create_evar_defs sigma =
+  mk_evar_defs (sigma,Metamap.empty)
+let evars_of d = d.evars
+let metas_of d = d.metas
+let evars_reset_evd evd d = {d with evars = evd}
+let reset_evd (sigma,mmap) d = {d with evars = sigma; metas=mmap}
+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, InternalHole)
+
+(* define the existential of section path sp as the constr body *)
+let evar_define sp body isevars =
+  (* needed only if an inferred type *)
+  let body = Termops.refresh_universes body in
+  {isevars with evars = define isevars.evars sp body}
+
+
+let evar_declare hyps evn ty ?(src=(dummy_loc,InternalHole)) evd =
+  { evd with
+    evars = add evd.evars evn
+      {evar_hyps=hyps; evar_concl=ty; evar_body=Evar_empty};
+    history = (evn,src)::evd.history }
+
+let set_evar_source ev k evd = {evd with history=(ev,k)::evd.history}
+
+let is_defined_evar isevars (n,_) = is_defined isevars.evars n
+
+(* Does k corresponds to an (un)defined existential ? *)
+let is_undefined_evar isevars c = match kind_of_term c with
+  | Evar ev -> not (is_defined_evar isevars ev)
+  | _ -> false
+
+
+let get_conv_pbs isevars p =
+  let (pbs,pbs1) = 
+    List.fold_left
+      (fun (pbs,pbs1) pb ->
+    	 if p pb then 
+	   (pb::pbs,pbs1)
+         else 
+	   (pbs,pb::pbs1))
+      ([],[])
+      isevars.conv_pbs
+  in
+  {isevars with conv_pbs = pbs1},
+  pbs
+
+let meta_defined evd mv =
+  match Metamap.find mv evd.metas with
     | Clval _ -> true
     | Cltyp _ -> false
  
-let meta_fvalue env mv =
-  match Metamap.find mv env with
+let meta_fvalue evd mv =
+  match Metamap.find mv evd.metas with
     | Clval(b,_) -> b
     | Cltyp _ -> anomaly "meta_fvalue: meta has no value"
            
-let meta_ftype env mv =
-  match Metamap.find mv env with
+let meta_ftype evd mv =
+  match Metamap.find mv evd.metas with
     | Cltyp b -> b
     | Clval(_,b) -> b
  
-let meta_declare mv v menv =
-  Metamap.add mv (Cltyp(mk_freelisted v)) menv
+let meta_declare mv v evd =
+  { evd with metas = Metamap.add mv (Cltyp(mk_freelisted v)) evd.metas }
   
-let meta_assign mv v menv =
-  Metamap.add mv (Clval(mk_freelisted v, meta_ftype menv mv)) menv
+let meta_assign mv v evd =
+  {evd with
+    metas =
+      Metamap.add mv (Clval(mk_freelisted v, meta_ftype evd mv)) evd.metas }
+
+let meta_merge evd1 evd2 =
+  {evd2 with
+    metas = List.fold_left (fun m (n,v) -> Metamap.add n v m) 
+      evd2.metas (metamap_to_list evd1.metas) }
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index df362a9bfa..fd6e944e14 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -9,9 +9,11 @@
 (*i $Id$ i*)
 
 (*i*)
+open Util
 open Names
 open Term
 open Sign
+open Libnames
 (*i*)
 
 (* The type of mappings for existential variables.
@@ -51,6 +53,7 @@ val is_evar : evar_map -> evar -> bool
 val is_defined : evar_map -> evar -> bool
 
 val evar_body : evar_info -> evar_body
+val evar_env :  evar_info -> Environ.env
 
 val string_of_existential : evar -> string
 val existential_of_int : int -> evar
@@ -104,8 +107,51 @@ type clbinding =
 val map_clb : (constr -> constr) -> clbinding -> clbinding
 
 type meta_map = clbinding Metamap.t
-val meta_defined : meta_map -> metavariable -> bool
-val meta_fvalue   : meta_map -> metavariable -> constr freelisted
-val meta_ftype    : meta_map -> metavariable -> constr freelisted
-val meta_declare : metavariable -> types -> meta_map -> meta_map
-val meta_assign  : metavariable -> constr -> meta_map -> meta_map
+
+(*************************)
+(* Unification state *)
+
+type hole_kind =
+  | ImplicitArg of global_reference * (int * identifier option)
+  | BinderType of name
+  | QuestionMark
+  | CasesType
+  | InternalHole
+  | TomatchTypeParameter of inductive * int
+
+type conv_pb = 
+  | CONV 
+  | CUMUL
+
+type evar_defs
+val evars_of : evar_defs -> evar_map
+val metas_of : evar_defs -> meta_map
+
+val mk_evar_defs :  evar_map * meta_map -> evar_defs
+(* the same with empty meta map: *)
+val create_evar_defs :  evar_map -> evar_defs
+val evars_reset_evd :  evar_map ->  evar_defs -> evar_defs
+val reset_evd :  evar_map * meta_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_constraint -> evar_defs -> evar_defs
+
+val evar_declare :
+  named_context -> evar -> types -> ?src:loc * hole_kind ->
+  evar_defs -> evar_defs
+val evar_define : evar -> constr -> evar_defs -> evar_defs
+
+val is_defined_evar :  evar_defs -> existential -> bool
+val is_undefined_evar :  evar_defs -> constr -> bool
+
+val get_conv_pbs : evar_defs -> (evar_constraint -> bool) -> 
+  evar_defs * evar_constraint list
+
+val meta_defined : evar_defs -> metavariable -> bool
+val meta_fvalue   : evar_defs -> metavariable -> constr freelisted
+val meta_ftype    : evar_defs -> metavariable -> constr freelisted
+val meta_declare : metavariable -> types -> evar_defs -> evar_defs
+val meta_assign  : metavariable -> constr -> evar_defs -> evar_defs
+
+val meta_merge : evar_defs -> evar_defs -> evar_defs
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 84fd4798b7..d3a602ac28 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -24,8 +24,8 @@ type pretype_error =
   | CantFindCaseType of constr
   (* Unification *)
   | OccurCheck of existential_key * constr
-  | NotClean of existential_key * constr * hole_kind
-  | UnsolvableImplicit of hole_kind
+  | NotClean of existential_key * constr * Evd.hole_kind
+  | UnsolvableImplicit of Evd.hole_kind
   | CannotUnify of constr * constr
   | CannotUnifyBindingType of constr * constr
   | CannotGeneralize of constr
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index fadd3f338f..ee4cdb2066 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -26,8 +26,8 @@ type pretype_error =
   | CantFindCaseType of constr
   (* Unification *)
   | OccurCheck of existential_key * constr
-  | NotClean of existential_key * constr * hole_kind
-  | UnsolvableImplicit of hole_kind
+  | NotClean of existential_key * constr * Evd.hole_kind
+  | UnsolvableImplicit of Evd.hole_kind
   | CannotUnify of constr * constr
   | CannotUnifyBindingType of constr * constr
   | CannotGeneralize of constr
@@ -84,9 +84,10 @@ val error_ill_typed_rec_body_loc :
 val error_occur_check : env ->  Evd.evar_map -> existential_key -> constr -> 'b
 
 val error_not_clean :
-  env ->  Evd.evar_map -> existential_key -> constr -> loc * hole_kind -> 'b
+  env -> Evd.evar_map -> existential_key -> constr -> loc * Evd.hole_kind -> 'b
 
-val error_unsolvable_implicit : loc -> env -> Evd.evar_map -> hole_kind -> 'b
+val error_unsolvable_implicit :
+  loc -> env -> Evd.evar_map -> Evd.hole_kind -> 'b
 
 val error_cannot_unify : env -> Evd.evar_map -> constr * constr -> 'b
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index d0402a552b..0054c4770b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -276,7 +276,7 @@ let rec pretype tycon env isevars lvar = function
   | RHole (loc,k) ->
       (match tycon with
 	 | Some ty ->
-	     { uj_val = e_new_isevar isevars env (loc,k) ty; uj_type = ty }
+	     { uj_val = e_new_evar isevars env ~src:(loc,k) ty; uj_type = ty }
 	 | None -> error_unsolvable_implicit loc env (evars_of !isevars) k)
 
   | RRec (loc,fixkind,names,bl,lar,vdef) ->
@@ -391,7 +391,7 @@ let rec pretype tycon env isevars lvar = function
 	
   | RLetIn(loc,name,c1,c2)      ->
       let j = pretype empty_tycon env isevars lvar c1 in
-      let t = Evarutil.refresh_universes j.uj_type in
+      let t = refresh_universes j.uj_type in
       let var = (name,Some j.uj_val,t) in
         let tycon = option_app (lift 1) tycon in
       let j' = pretype tycon (push_rel var env) isevars lvar c2 in
@@ -529,7 +529,7 @@ let rec pretype tycon env isevars lvar = function
 		   Cases.pred_case_ml 
 		     env (evars_of !isevars) false indt (0,fj.uj_type) 
 		 in 
-		 if has_undefined_isevars !isevars pred then
+		 if has_undefined_evars !isevars pred then
 		   use_constraint ()
 		 else
 		   true, pred
@@ -683,7 +683,8 @@ let rec pretype tycon env isevars lvar = function
 	| None -> 
 	    let p = match tycon with
 	    | Some ty -> ty
-	    | None -> e_new_isevar isevars env (loc,InternalHole) (new_Type ())
+	    | None ->
+                e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ())
 	    in
 	    it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
       let f cs b =
@@ -750,7 +751,7 @@ let rec pretype tycon env isevars lvar = function
 		  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)
+		  if has_undefined_evars !isevars pred then findtype (i+1)
 		  else 
 		    let pty =
                       Retyping.get_type_of env (evars_of !isevars) pred in
@@ -942,7 +943,7 @@ and pretype_type valcon env isevars lvar = function
 	       utj_type = s }
 	 | None ->
 	     let s = new_Type_sort () in
-	     { utj_val = e_new_isevar isevars env loc (mkSort s);
+	     { utj_val = e_new_evar isevars env ~src:loc (mkSort s);
 	       utj_type = s})
   | c ->
       let j = pretype empty_tycon env isevars lvar c in
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 1aeca07cb7..0a9722b878 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -15,6 +15,7 @@ open Sign
 open Term
 open Libnames
 open Nametab
+open Evd
 (*i*)
 
 (* Untyped intermediate terms, after ASTs and before constr. *)
@@ -48,14 +49,6 @@ type 'a bindings =
 
 type 'a with_bindings = 'a * 'a bindings
 
-type hole_kind =
-  | ImplicitArg of global_reference * (int * identifier option)
-  | BinderType of name
-  | QuestionMark
-  | CasesType
-  | InternalHole
-  | TomatchTypeParameter of inductive * int
-
 type rawconstr = 
   | RRef of (loc * global_reference)
   | RVar of (loc * identifier)
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 54bb306bd0..ff1f86c58a 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -46,14 +46,6 @@ type 'a bindings =
 
 type 'a with_bindings = 'a * 'a bindings
 
-type hole_kind =
-  | ImplicitArg of global_reference * (int * identifier option)
-  | BinderType of name
-  | QuestionMark
-  | CasesType
-  | InternalHole
-  | TomatchTypeParameter of inductive * int
-
 type rawconstr = 
   | RRef of (loc * global_reference)
   | RVar of (loc * identifier)
@@ -74,7 +66,7 @@ type rawconstr =
   | RRec of loc * fix_kind * identifier array * rawdecl list array *
       rawconstr array * rawconstr array
   | RSort of loc * rawsort
-  | RHole of (loc * hole_kind)
+  | RHole of (loc * Evd.hole_kind)
   | RCast of loc * rawconstr * rawconstr
   | RDynamic of loc * Dyn.t
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index a9fc90df26..9372effebd 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -461,10 +461,6 @@ let fhnf_apply info k h a = Profile.profile4 fakey fhnf_apply info k h a;;
 
 type conversion_test = constraints -> constraints
 
-type conv_pb = 
-  | CONV 
-  | CUMUL
-
 let pb_is_equal pb = pb = CONV
 
 let pb_equal = function
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index b02cc42145..9c70b1a404 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -162,10 +162,6 @@ val reduce_fix : local_state_reduction_function -> fixpoint
 
 type conversion_test = constraints -> constraints
 
-type conv_pb = 
-  | CONV 
-  | CUMUL
-
 val pb_is_equal : conv_pb -> bool
 val pb_equal : conv_pb -> conv_pb
 
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 18c54da47e..f0c01a56ec 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -9,12 +9,9 @@
 (*i $Id$ i*)
 
 (*i*)
-open Names
 open Term
 open Evd
 open Environ
-open Pattern
-open Termops
 (*i*)
 
 (* This family of functions assumes its constr argument is known to be
@@ -23,11 +20,12 @@ open Termops
    either produces a wrong result or raise an anomaly. Use with care.
    It doesn't handle predicative universes too. *)
 
-val get_type_of : env -> evar_map -> constr -> constr
+val get_type_of : env -> evar_map -> constr -> types
 val get_sort_of : env -> evar_map -> types -> sorts
 val get_sort_family_of : env -> evar_map -> types -> sorts_family
 
-val get_type_of_with_meta : env -> evar_map -> metamap -> constr -> constr
+val get_type_of_with_meta :
+  env -> evar_map -> Termops.metamap -> constr -> types
 
 (* Makes an assumption from a constr *)
 val get_assumption_of : env -> evar_map -> constr -> types
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 02e8618dc5..d8c85cf7af 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -101,6 +101,20 @@ let new_univ =
   (fun sp ->
     incr univ_gen; 
     Univ.make_univ (Lib.library_dp(),!univ_gen))
+let new_Type () = mkType (new_univ ())
+let new_Type_sort () = Type (new_univ ())
+
+(* This refreshes universes in types; works only for inferred types (i.e. for
+   types of the form (x1:A1)...(xn:An)B with B a sort or an atom in
+   head normal form) *)
+let refresh_universes t =
+  let modified = ref false in
+  let rec refresh t = match kind_of_term t with
+    | Sort (Type _) -> modified := true; new_Type ()
+    | Prod (na,u,v) -> mkProd (na,u,refresh v)
+    | _ -> t in
+  let t' = refresh t in
+  if !modified then t' else t
 
 let new_sort_in_family = function 
   | InProp -> mk_Prop
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 8ce7b39dcb..e1a9d5ba95 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -19,6 +19,9 @@ open Environ
 (*val set_module : Names.dir_path -> unit*)
 val new_univ : unit -> Univ.universe
 val new_sort_in_family : sorts_family -> sorts
+val new_Type : unit -> types
+val new_Type_sort : unit -> sorts
+val refresh_universes : types -> types
 
 (* printers *)
 val print_sort : sorts -> std_ppcmds
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index b98ff0e7dc..9aa2758a03 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -24,23 +24,24 @@ let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t)
 (* The typing machine without information, without universes but with
    existential variables. *)
 
-let assumption_of_judgment env (sigma,_) j =
-  assumption_of_judgment env (j_nf_evar sigma j)
+let assumption_of_judgment env evd j =
+  assumption_of_judgment env (j_nf_evar (Evd.evars_of evd) j)
 
-let type_judgment env (sigma,_) j =
-  type_judgment env (j_nf_evar sigma j)
+let type_judgment env evd j =
+  type_judgment env (j_nf_evar (Evd.evars_of evd) j)
 
-let check_type env (sigma,_) j ty =
+let check_type env evd j ty =
+  let sigma = Evd.evars_of evd in
   if not (is_conv_leq env sigma j.uj_type ty) then
     error_actual_type env (j_nf_evar sigma j) (nf_evar sigma ty)
 
 let rec execute env evd cstr =
   match kind_of_term cstr with
     | Meta n ->
-        { uj_val = cstr; uj_type = Evarutil.meta_type (snd evd) n }
+        { uj_val = cstr; uj_type = Evarutil.meta_type evd n }
 
     | Evar ev ->
-        let sigma = fst evd in
+        let sigma = Evd.evars_of evd in
 	let ty = Evd.existential_type sigma ev in
 	let jty = execute env evd ty in
 	let jty = assumption_of_judgment env evd jty in
@@ -161,11 +162,11 @@ let msort_of env evd c =
   a.utj_type
 
 let type_of env sigma c =
-  mtype_of env (sigma, Evd.Metamap.empty) c
+  mtype_of env (Evd.create_evar_defs sigma) c
 let sort_of env sigma c =
-  msort_of env (sigma, Evd.Metamap.empty) c
+  msort_of env (Evd.create_evar_defs sigma) c
 let check env sigma c   =
-  mcheck env (sigma, Evd.Metamap.empty) c
+  mcheck env (Evd.create_evar_defs sigma) c
 
 (* The typed type of a judgment. *)
 
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 15f3a6597a..c4503f51bd 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -25,9 +25,9 @@ val sort_of : env -> evar_map -> types -> sorts
 val check   : env -> evar_map -> constr -> types -> unit
  
 (* The same but with metas... *)
-val mtype_of : env -> evar_map * meta_map -> constr -> types
-val msort_of : env -> evar_map * meta_map -> types -> sorts
-val mcheck   : env -> evar_map * meta_map -> constr -> types -> unit
+val mtype_of : env -> evar_defs -> constr -> types
+val msort_of : env -> evar_defs -> types -> sorts
+val mcheck   : env -> evar_defs -> constr -> types -> unit
  
 (* unused typing function... *)
-val mtype_of_type : env -> evar_map * meta_map -> types -> types
+val mtype_of_type : env -> evar_defs -> types -> types
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 33f09fd0a7..11b24f0964 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -51,7 +51,7 @@ let abstract_list_all env sigma typ c l =
 
 let w_Declare env sp ty evd =
   let sigma = evars_of evd in
-  let _ = Typing.type_of env sigma ty in (* Utile ?? *)
+  let _ = Typing.type_of env sigma ty in (* Checks there is no meta *)
   let newdecl =
     { evar_hyps=named_context env; evar_concl=ty; evar_body=Evar_empty } in 
   evars_reset_evd (Evd.add sigma sp newdecl) evd
@@ -211,9 +211,7 @@ let applyHead env evd n c  =
     else 
       match kind_of_term (whd_betadeltaiota env (evars_of evd) cty) with
         | Prod (_,c1,c2) ->
-            let (evd',evar) =
-              Evarutil.new_isevar evd env
-                (dummy_loc,Rawterm.InternalHole) c1 in
+            let (evd',evar) = Evarutil.new_evar evd env c1 in
 	    apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd'
 	| _ -> error "Apply_Head_Then"
   in 
@@ -270,25 +268,23 @@ let w_merge env with_types metas evars evd =
 	  | _ -> anomaly "w_merge_rec"))
 
       | ([], (mv,n)::t) ->
-          let mmap = metas_of evd in
-    	  if meta_defined mmap mv then
+    	  if meta_defined evd mv then
             let (metas',evars') =
-              unify_0 env (evars_of evd) CONV (meta_fvalue mmap mv).rebus n in
+              unify_0 env (evars_of evd) CONV (meta_fvalue evd mv).rebus n in
             w_merge_rec evd (metas'@t) evars'
     	  else
             begin
 	      if with_types (* or occur_meta mvty *) then
-	        (let mvty = meta_type mmap mv in
+	        (let mvty = meta_type evd 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 evd 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 -> ());
-              let evd' =
-                reset_evd (evars_of evd,meta_assign mv n mmap) evd in
+              let evd' = meta_assign mv n evd in
 	      w_merge_rec evd' t []
             end
 
@@ -430,7 +426,7 @@ let secondOrderAbstraction env allow_K typ (p, oplist) evd =
   let sigma = evars_of evd in
   let (evd',cllist) =
     w_unify_to_subterm_list env allow_K oplist typ evd in
-  let typp = meta_type (metas_of evd') p in
+  let typp = meta_type evd' p in
   let pred = abstract_list_all env sigma typp typ cllist in
   w_unify_0 env CONV (mkMeta p) pred evd'
 
@@ -443,13 +439,13 @@ let w_unify2 env allow_K cv_pb ty1 ty2 evd =
 	let evd' =
           secondOrderAbstraction env allow_K ty2 (p1,oplist1) evd in 
         (* Resume first order unification *)
-	w_unify_0 env cv_pb (nf_meta (metas_of evd') ty1) ty2 evd'
+	w_unify_0 env cv_pb (nf_meta evd' ty1) ty2 evd'
     | _, Meta p2 ->
         (* Find the predicate *)
 	let evd' =
           secondOrderAbstraction env allow_K ty1 (p2, oplist2) evd in 
         (* Resume first order unification *)
-	w_unify_0 env cv_pb ty1 (nf_meta (metas_of evd') ty2) evd'
+	w_unify_0 env cv_pb ty1 (nf_meta evd' ty2) evd'
     | _ -> error "w_unify2"
 
 
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index d3007e69df..95b35a56ca 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -23,8 +23,7 @@ val w_Define : evar -> constr -> evar_defs -> evar_defs
 
 (* The "unique" unification fonction *)
 val w_unify :
-  bool -> env -> Reductionops.conv_pb -> constr -> constr ->
-  evar_defs -> evar_defs
+  bool -> env -> conv_pb -> constr -> constr -> evar_defs -> evar_defs
 
 (* [w_unify_to_subterm env (c,t) m] performs unification of [c] with a
    subterm of [t]. Constraints are added to [m] and the matched