inclusion de meta_map dans evar_defs

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

9 files changed, 203 insertions, 183 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 45ead5a9f..5b4ed6571 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -27,65 +27,47 @@ open Evarutil
 open Unification
 
 (* *)
-let w_coerce wc c ctyp target =
+let w_coerce env c ctyp target evd =
   let j = make_judge c ctyp in
-  let env = Global.env_of_context wc.it in
-  let isevars = create_evar_defs wc.sigma in
-  let (evd',j') = Coercion.inh_conv_coerce_to dummy_loc env isevars j target in
-  (evars_of evd',j'.uj_val)
+  let (evd',j') = Coercion.inh_conv_coerce_to dummy_loc env evd j target in
+  (evd',j'.uj_val)
 
 let pf_env gls = Global.env_of_context gls.it.evar_hyps
 let pf_type_of gls c  = Typing.type_of (pf_env gls) gls.sigma c
 let pf_hnf_constr gls c = hnf_constr (pf_env gls) gls.sigma c
 let pf_concl gl = gl.it.evar_concl
 
-(* Generator of metavariables *)
-let new_meta =
-  let meta_ctr = ref 0 in
-  fun () -> incr meta_ctr; !meta_ctr
-
-(* replaces a mapping of existentials into a mapping of metas.
-   Problem if an evar appears in the type of another one (pops anomaly) *)
-let exist_to_meta sigma (emap, c) =
-  let metamap = ref [] in
-  let change_exist evar =
-    let ty = nf_betaiota (nf_evar emap (existential_type emap evar)) in
-    let n = new_meta() in
-    metamap := (n, ty) :: !metamap;
-    mkMeta n in
-  let rec replace c =
-    match kind_of_term c with
-        Evar (k,_ as ev) when not (Evd.in_dom sigma k) -> change_exist ev
-      | _ -> map_constr replace c in
-  (!metamap, replace c)
-
 (******************************************************************)
 (* Clausal environments *)
 
-type wc = named_context sigma
-
 type clausenv = {
+  templenv : env;
+  env      : evar_defs;
   templval : constr freelisted;
   templtyp : constr freelisted;
-  namenv : identifier Metamap.t;
-  env : meta_map;
-  hook : wc }
+  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 f sub clenv = 
+let subst_clenv sub clenv = 
   { templval = map_fl (subst_mps sub) clenv.templval;
     templtyp = map_fl (subst_mps sub) clenv.templtyp;
     namenv = clenv.namenv;
-    env = Metamap.map (map_clb (subst_mps sub)) clenv.env;
-    hook = f sub clenv.hook }
+    env = reset_evd
+      (evars_of clenv.env,
+       Metamap.map (map_clb (subst_mps sub)) (cl_metas clenv))
+      clenv.env;
+    templenv = clenv.templenv }
 
-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_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 cl_env ce = Global.env_of_context ce.hook.it
 
-let clenv_hnf_constr ce t = hnf_constr (cl_env ce) ce.hook.sigma t
+let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
 
 let clenv_get_type_of ce c =
   let metamap =
@@ -93,8 +75,8 @@ let clenv_get_type_of ce c =
       (function
 	 | (n,Clval(_,typ)) -> (n,typ.rebus)
          | (n,Cltyp typ)    -> (n,typ.rebus))
-      (metamap_to_list ce.env) in
-  Retyping.get_type_of_with_meta (cl_env ce) ce.hook.sigma metamap c
+      (metamap_to_list (cl_metas ce)) in
+  Retyping.get_type_of_with_meta (cl_env ce) (cl_sigma ce) metamap c
 
 
 
@@ -120,7 +102,7 @@ let clenv_environments bound c =
             else 
 	      ne 
 	  in
-	  let e' = Metamap.add mv (Cltyp (mk_freelisted c1)) e in 
+	  let e' = meta_declare mv c1 e in
 	  clrec (ne',e', (mkMeta mv)::metas) (option_app ((+) (-1)) n)
 	    (if dep then (subst1 (mkMeta mv) c2) else c2)
       | (n, LetIn (na,b,_,c)) ->
@@ -134,8 +116,8 @@ let mk_clenv_from_n gls n (c,cty) =
   { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args));
     templtyp = mk_freelisted concl;
     namenv = namenv;
-    env = env;
-    hook = {it=gls.it.evar_hyps; sigma=gls.sigma} }
+    env = mk_evar_defs (gls.sigma,env);
+    templenv = Global.env_of_context gls.it.evar_hyps }
 
 let mk_clenv_from gls = mk_clenv_from_n gls None
 
@@ -156,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 clenv.env with
+     (match Metamap.find mv1 (cl_metas clenv) with
 	 | Clval (b,_) -> 
 	     Metaset.mem mv0 b.freemetas || meta_exists menrec b.freemetas
 	 | Cltyp _ -> false)
@@ -165,7 +147,7 @@ let mentions clenv mv0 =
   in 
   menrec
 
-let clenv_defined clenv mv = meta_defined clenv.env mv
+let clenv_defined clenv mv = meta_defined (cl_metas clenv) mv
 
 (* TODO: replace by clenv_unify (mkMeta mv) rhs ? *)		      
 let clenv_assign mv rhs clenv =
@@ -173,11 +155,10 @@ 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 clenv.env with
+    (match Metamap.find mv (cl_metas clenv) with
        | Clval (fls,ty) ->
 	   if not (eq_constr fls.rebus rhs) then
 	     try 
-	       (* Streams are lazy, force evaluation of id to catch Not_found*)
 	       let id = Metamap.find mv clenv.namenv in
 	       errorlabstrm "clenv_assign"
 		 (str "An incompatible instantiation has already been found for " ++ 
@@ -187,19 +168,16 @@ let clenv_assign mv rhs clenv =
 	   else
 	     clenv
        | Cltyp bty -> 
-	   { templval = clenv.templval;
-	     templtyp = clenv.templtyp;
-	     namenv = clenv.namenv;
-	     env = Metamap.add mv (Clval (rhs_fls,bty)) clenv.env;
-	     hook = clenv.hook })
+	   { clenv with
+	     env = reset_evd
+               (cl_sigma clenv,
+                Metamap.add mv (Clval (rhs_fls,bty)) (cl_metas clenv))
+               clenv.env })
   with Not_found -> 
     error "clenv_assign"
 
 
-let clenv_wtactic f clenv =
-  let (evd',mmap') =
-    f (create_evar_defs clenv.hook.sigma, clenv.env) in
-  {clenv with env = mmap' ; hook = {it=clenv.hook.it; sigma=evars_of evd'}}
+let clenv_wtactic f clenv = {clenv with env = f clenv.env }
 
 
 (* [clenv_dependent hyps_only clenv]
@@ -225,7 +203,7 @@ 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 clenv.env mv).freemetas
+let clenv_metavars clenv mv = (meta_ftype (cl_metas clenv) mv).freemetas
 
 let dependent_metas clenv mvs conclmetas =
   List.fold_right
@@ -247,8 +225,7 @@ let clenv_missing ce = clenv_dependent true ce
 (******************************************************************)
 
 let clenv_unify allow_K cv_pb t1 t2 clenv =
-  let env = cl_env clenv in
-  clenv_wtactic (w_unify allow_K env cv_pb t1 t2) clenv
+  { clenv with env = w_unify allow_K clenv.templenv cv_pb t1 t2 clenv.env }
 
 let clenv_unique_resolver allow_K clause gl =
   clenv_unify allow_K CUMUL (clenv_type clause) (pf_concl gl) clause 
@@ -279,8 +256,9 @@ let evar_clenv_unique_resolver clenv gls =
 (******************************************************************)
 
 let connect_clenv gls clenv =
-  let wc = {it=gls.it.evar_hyps; sigma=gls.sigma} in
-  { clenv with hook = wc }
+  { clenv with
+    env = evars_reset_evd gls.sigma clenv.env;
+    templenv = Global.env_of_context gls.it.evar_hyps }
 
 (* [clenv_fchain mv clenv clenv']
  *
@@ -308,9 +286,12 @@ let clenv_fchain mv clenv nextclenv =
 			  end else 
 			    Metamap.add mv id ne)
           clenv.namenv (metamap_to_list nextclenv.namenv);
-      env = List.fold_left (fun m (n,v) -> Metamap.add n v m) 
-	       clenv.env (metamap_to_list nextclenv.env);
-      hook = nextclenv.hook } 
+      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;
+      templenv = nextclenv.templenv } 
   in
   (* unify the type of the template of [nextclenv] with the type of [mv] *)
   let clenv'' =
@@ -390,11 +371,11 @@ let clenv_match_args s clause =
 	  with _ ->
 	  (* Try to coerce to the type of [k]; cannot merge with the
 	     previous case because Coercion does not handle Meta *)
-          let (_,c') = w_coerce clause.hook c c_typ k_typ in
-	  try clenv_unify true CONV (mkMeta k) c' clause
-	  with PretypeError (env,CannotUnify (m,n)) ->
-	    Stdpp.raise_with_loc loc
- 	      (PretypeError (env,CannotUnifyBindingType (m,n)))
+            let (_,c') = w_coerce (cl_env clause) c c_typ k_typ clause.env in
+	    try clenv_unify true CONV (mkMeta k) c' clause
+	    with PretypeError (env,CannotUnify (m,n)) ->
+	      Stdpp.raise_with_loc loc
+ 	        (PretypeError (env,CannotUnifyBindingType (m,n)))
 	in matchrec cl t
   in 
   matchrec clause s
@@ -435,14 +416,13 @@ let clenv_constrain_dep_args hyps_only clause = function
       if List.length occlist = List.length mlist then
 	List.fold_left2
           (fun clenv k c ->
-	    let wc = clause.hook in
 	    try
 	      let k_typ =
                 clenv_hnf_constr clause (clenv_meta_type clause k) in
 	      let c_typ =
                 clenv_hnf_constr clause (clenv_get_type_of clause c) in
               (* faire quelque chose avec le sigma retourne ? *)
-	      let (_,c') = w_coerce wc c c_typ k_typ in
+	      let (_,c') = w_coerce (cl_env clenv) c c_typ k_typ clenv.env in
 	      clenv_unify true CONV (mkMeta k) c' clenv
 	    with _ ->
               clenv_unify true CONV (mkMeta k) c clenv)
@@ -494,4 +474,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 clenv.env)))
+     (prlist pr_meta_binding (metamap_to_list (cl_metas clenv))))
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index 375d84eac..30bc96338 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -13,40 +13,31 @@ open Util
 open Names
 open Term
 open Sign
+open Environ
 open Evd
 open Evarutil
 (*i*)
 
-(* [new_meta] is a generator of unique meta variables *)
-val new_meta : unit -> metavariable
-
-(* [exist_to_meta] generates new metavariables for each existential
-   and performs the replacement in the given constr *)
-val exist_to_meta :
-  evar_map -> Pretyping.open_constr -> (Termops.metamap * constr)
-
 (***************************************************************)
 (* The Type of Constructions clausale environments. *)
 
-(* [templval] is the template which we are trying to fill out.
+(* [templenv] is the typing context
+ * [env] is the mapping from metavar and evar numbers to their types
+ *       and values.
+ * [templval] is the template which we are trying to fill out.
  * [templtyp] is its type.
  * [namenv] is a mapping from metavar numbers to names, for
  *          use in instanciating metavars by name.
- * [evd] is the mapping from metavar and evar numbers to their types
- *       and values.
- * [hook] is a signature (named_context) and a sigma: the
- *        typing context
  *)
-type wc = named_context sigma (* for a better reading of the following *)
 type clausenv = {
+  templenv : env;
+  env      : evar_defs;
   templval : constr freelisted;
   templtyp : constr freelisted;
-  namenv : identifier Metamap.t;
-  env : meta_map;
-  hook : wc }
+  namenv   : identifier Metamap.t }
 
-val subst_clenv :
-  (substitution -> wc -> wc) -> substitution -> clausenv -> clausenv
+(* Substitution is not applied neither to the evar_map of evar_defs nor hook *)
+val subst_clenv : substitution -> clausenv -> clausenv
 
 (* subject of clenv (instantiated) *)
 val clenv_value     : clausenv -> constr
@@ -118,9 +109,3 @@ val make_clenv_binding :
 (* Pretty-print *)
 val pr_clenv : clausenv -> Pp.std_ppcmds
 
-(***************************************************************)
-(* Old or unused stuff... *)
-
-val clenv_wtactic :
-  (evar_defs * meta_map -> evar_defs * meta_map) -> clausenv -> clausenv
-
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 9a4c9cfed..cb4efd2e1 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -92,6 +92,63 @@ let nf_evar_info evc info =
     evar_body = info.evar_body}
 
 (**********************)
+(* Creating new metas *)
+(**********************)
+
+(* Generator of metavariables *)
+let new_meta =
+  let meta_ctr = ref 0 in
+  fun () -> incr meta_ctr; !meta_ctr
+
+let mk_new_meta () = mkMeta(new_meta())
+
+(* replaces a mapping of existentials into a mapping of metas.
+   Problem if an evar appears in the type of another one (pops anomaly) *)
+let exist_to_meta sigma (emap, c) =
+  let metamap = ref [] in
+  let change_exist evar =
+    let ty = nf_betaiota (nf_evar emap (existential_type emap evar)) in
+    let n = new_meta() in
+    metamap := (n, ty) :: !metamap;
+    mkMeta n in
+  let rec replace c =
+    match kind_of_term c with
+        Evar (k,_ as ev) when not (Evd.in_dom sigma k) -> change_exist ev
+      | _ -> map_constr replace c in
+  (!metamap, replace c)
+
+(*************************************)
+(* Metas *)
+
+let meta_val_of env mv = 
+  let rec valrec mv =
+    try
+      (match Metamap.find mv env with
+	 | Cltyp _ -> mkMeta mv
+	 | Clval(b,_) ->
+	     instance (List.map (fun mv' -> (mv',valrec mv')) 
+			       (Metaset.elements b.freemetas)) b.rebus)
+    with Not_found -> 
+      mkMeta mv
+  in 
+  valrec mv
+
+let meta_instance env b =
+  let c_sigma =
+    List.map 
+      (fun mv -> (mv,meta_val_of env mv)) (Metaset.elements b.freemetas)
+  in 
+  instance c_sigma b.rebus
+
+let nf_meta env c = meta_instance env (mk_freelisted c)
+
+let meta_type env mv =
+  let ty =
+    try meta_ftype env mv
+    with Not_found -> error ("unknown meta ?"^string_of_int mv) in
+  meta_instance env ty
+
+(**********************)
 (* Creating new evars *)
 (**********************)
 
@@ -216,15 +273,22 @@ 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 }
+      history : (existential_key * (loc * Rawterm.hole_kind)) list;
+      metas : Evd.meta_map }
 
-let create_evar_defs evd = { evars=evd; conv_pbs=[]; history=[] }
+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
@@ -594,33 +658,3 @@ let valcon_of_tycon x = x
 
 let lift_tycon = option_app (lift 1)
 
-(*************************************)
-(* Metas *)
-
-let meta_val_of env mv = 
-  let rec valrec mv =
-    try
-      (match Metamap.find mv env with
-	 | Cltyp _ -> mkMeta mv
-	 | Clval(b,_) ->
-	     instance (List.map (fun mv' -> (mv',valrec mv')) 
-			       (Metaset.elements b.freemetas)) b.rebus)
-    with Not_found -> 
-      mkMeta mv
-  in 
-  valrec mv
-
-let meta_instance env b =
-  let c_sigma =
-    List.map 
-      (fun mv -> (mv,meta_val_of env mv)) (Metaset.elements b.freemetas)
-  in 
-  instance c_sigma b.rebus
-
-let nf_meta env c = meta_instance env (mk_freelisted c)
-
-let meta_type env mv =
-  let ty =
-    try meta_ftype env mv
-    with Not_found -> error ("unknown meta ?"^string_of_int mv) in
-  meta_instance env ty
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 4223b0e78..6d264b718 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -40,19 +40,40 @@ exception Uninstantiated_evar of existential_key
 val whd_ise :  evar_map -> constr -> constr
 val whd_castappevar :  evar_map -> constr -> constr
 
+(***********************************************************)
+(* Metas *)
+
+(* [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
+
+(* [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 evars_of : evar_defs -> evar_map
+val metas_of : evar_defs -> meta_map
 
 val non_instantiated : evar_map -> (evar * evar_info) list
 
-val create_evar_defs :  evar_map ->  evar_defs
+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
@@ -82,6 +103,7 @@ val solve_simple_eqn :
 val define_evar_as_arrow : evar_defs -> existential -> evar_defs * types
 val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts
 
+(***********************************************************)
 (* Value/Type constraints *)
 
 val new_Type_sort : unit -> sorts
@@ -105,7 +127,3 @@ val valcon_of_tycon : type_constraint -> val_constraint
 
 val lift_tycon : type_constraint -> type_constraint
 
-(* Metas *)
-val nf_meta       : meta_map -> constr -> constr
-val meta_type     : meta_map -> metavariable -> types
-val meta_instance : meta_map -> constr freelisted -> constr
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index be35cb947..d7468eded 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -118,6 +118,9 @@ let existential_opt_value sigma ev =
   with NotInstantiatedEvar -> None
 
 (*******************************************************************)
+type open_constr = evar_map * constr
+
+(*******************************************************************)
 (* The type constructor ['a sigma] adds an evar map to an object of
   type ['a] *)
 type 'a sigma = {
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 3f9eaa5fa..df362a9bf 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -64,6 +64,10 @@ val existential_type : evar_map -> existential -> types
 val existential_opt_value : evar_map -> existential -> constr option
 
 (*************************)
+(* constr with holes *)
+type open_constr = evar_map * constr
+
+(*************************)
 (* The type constructor ['a sigma] adds an evar map to an object of
   type ['a] *)
 type 'a sigma = {
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 57a3d1be8..096c982c5 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -20,10 +20,6 @@ open Evarutil
 
 type var_map = (identifier * unsafe_judgment) list
 
-(* constr with holes *)
-type open_constr = evar_map * constr
-
-
 (* Generic call to the interpreter from rawconstr to constr, failing
    unresolved holes in the rawterm cannot be instantiated.
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 4a9cab206..33f09fd0a 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -49,14 +49,12 @@ let abstract_list_all env sigma typ c l =
 
 (*******************************)
 
-type maps = evar_defs * meta_map
-
-let w_Declare env sp ty (evd,mmap) =
+let w_Declare env sp ty evd =
   let sigma = evars_of evd in
   let _ = Typing.type_of env sigma ty in (* Utile ?? *)
   let newdecl =
     { evar_hyps=named_context env; evar_concl=ty; evar_body=Evar_empty } in 
-  (evars_reset_evd (Evd.add sigma sp newdecl) evd, mmap)
+  evars_reset_evd (Evd.add sigma sp newdecl) evd
 
 (* [w_Define evd sp c]
  *
@@ -66,7 +64,7 @@ let w_Declare env sp ty (evd,mmap) =
  * No unification is performed in order to assert that [c] has the
  * correct type.
  *)
-let w_Define sp c (evd,mmap) =
+let w_Define sp c evd =
   let sigma = evars_of evd in
   if Evd.is_defined sigma sp then
     error "Unify.w_Define: cannot define evar twice";
@@ -82,7 +80,7 @@ let w_Define sp c (evd,mmap) =
       (str "Cannot use variable " ++ pr_id v ++ str " to define " ++ 
        str (string_of_existential sp)) in
   let spdecl' = { spdecl with evar_body = Evar_defined c } in
-  (evars_reset_evd (Evd.add sigma sp spdecl') evd, mmap)
+  evars_reset_evd (Evd.add sigma sp spdecl') evd
 
 
 (* Unification à l'ordre 0 de m et n: [unify_0 env sigma cv_pb m n]
@@ -230,17 +228,17 @@ let is_mimick_head f =
    or in evars, possibly generating new unification problems; if [b]
    is true, unification of types of metas is required *)
 
-let w_merge env with_types metas evars maps =
+let w_merge env with_types metas evars evd =
   let ty_metas = ref [] in
   let ty_evars = ref [] in
-  let rec w_merge_rec (evd,mmap as maps) metas evars =
+  let rec w_merge_rec evd metas evars =
     match (evars,metas) with
-      | ([], []) -> maps
+      | ([], []) -> evd
 
       | ((lhs,rhs)::t, metas) ->
       (match kind_of_term rhs with
 
-	| Meta k -> w_merge_rec maps ((k,lhs)::metas) t
+	| Meta k -> w_merge_rec evd ((k,lhs)::metas) t
 
 	| krhs ->
         (match kind_of_term lhs with
@@ -249,7 +247,7 @@ let w_merge env with_types metas evars maps =
     	      if is_defined_evar evd ev then
 		let (metas',evars') =
                   unify_0 env (evars_of evd) CONV rhs lhs in
-		w_merge_rec maps (metas'@metas) (evars'@t)
+		w_merge_rec evd (metas'@metas) (evars'@t)
     	      else begin
 		let rhs' = 
 		  if occur_meta rhs then subst_meta metas rhs else rhs 
@@ -259,23 +257,24 @@ let w_merge env with_types metas evars maps =
                 match krhs with
 		  | App (f,cl) when is_mimick_head f ->
 		      (try 
-		        w_merge_rec (w_Define evn rhs' maps) metas t
+		        w_merge_rec (w_Define evn rhs' evd) metas t
 		      with ex when precatchable_exception ex ->
-                        let maps' =
-                          mimick_evar maps f (Array.length cl) evn in
-			w_merge_rec maps' metas evars)
+                        let evd' =
+                          mimick_evar evd f (Array.length cl) evn in
+			w_merge_rec evd' metas evars)
                   | _ ->
                       (* ensure tail recursion in non-mimickable case! *)
-		      w_merge_rec (w_Define evn rhs' maps) metas t
+		      w_merge_rec (w_Define evn rhs' evd) metas t
 	      end
 
 	  | _ -> anomaly "w_merge_rec"))
 
       | ([], (mv,n)::t) ->
+          let mmap = metas_of evd in
     	  if meta_defined mmap mv then
             let (metas',evars') =
               unify_0 env (evars_of evd) CONV (meta_fvalue mmap mv).rebus n in
-            w_merge_rec maps (metas'@t) evars'
+            w_merge_rec evd (metas'@t) evars'
     	  else
             begin
 	      if with_types (* or occur_meta mvty *) then
@@ -288,30 +287,31 @@ let w_merge env with_types metas evars maps =
                   ty_metas := mc @ !ty_metas;
                   ty_evars := ec @ !ty_evars
 		with e when precatchable_exception e -> ());
-              let mmap' = meta_assign mv n mmap in
-	      w_merge_rec (evd,mmap') t []
+              let evd' =
+                reset_evd (evars_of evd,meta_assign mv n mmap) evd in
+	      w_merge_rec evd' t []
             end
 
-  and mimick_evar (evd,mmap) hdc nargs sp =
+  and mimick_evar evd hdc nargs sp =
     let ev = Evd.map (evars_of evd) sp in
     let sp_env = Global.env_of_context ev.evar_hyps in
     let (evd', c) = applyHead sp_env evd nargs hdc in
     let (mc,ec) =
       unify_0 sp_env (evars_of evd') CUMUL
         (Retyping.get_type_of sp_env (evars_of evd') c) ev.evar_concl in
-    let maps' = w_merge_rec (evd',mmap) mc ec in
-    if (evars_of evd') == (evars_of (fst maps'))
-    then w_Define sp c maps'
-    else w_Define sp (Evarutil.nf_evar (evars_of (fst maps')) c) maps' in
+    let evd'' = w_merge_rec evd' mc ec in
+    if (evars_of evd') == (evars_of evd'')
+    then w_Define sp c evd''
+    else w_Define sp (Evarutil.nf_evar (evars_of evd'') c) evd'' in
 
   (* merge constraints *)
-  let maps' = w_merge_rec maps metas evars in
+  let evd' = w_merge_rec evd metas evars in
   if with_types then
     (* merge constraints about types: if they fail, don't worry *)
-    try w_merge_rec maps' !ty_metas !ty_evars
-    with e when precatchable_exception e -> maps'
+    try w_merge_rec evd' !ty_metas !ty_evars
+    with e when precatchable_exception e -> evd'
   else
-    maps'
+    evd'
 
 (* [w_unify env evd M N]
    performs a unification of M and N, generating a bunch of
@@ -324,7 +324,7 @@ let w_merge env with_types metas evars maps =
    types of metavars are unifiable with the types of their instances    *)
 
 let w_unify_core_0 env with_types cv_pb m n evd =
-  let (mc,ec) = unify_0 env (evars_of (fst evd)) cv_pb m n in 
+  let (mc,ec) = unify_0 env (evars_of evd) cv_pb m n in 
   w_merge env with_types mc ec evd
 
 let w_unify_0 env = w_unify_core_0 env false
@@ -418,19 +418,19 @@ let w_unify_to_subterm_list env allow_K oplist t evd =
           with PretypeError (env,NoOccurrenceFound _) when allow_K -> (evd,op)
         in 
 	(evd',cl::l)
-      else if not allow_K & not (dependent op t) then
-	(* This is not up to delta ... *)
-	raise (PretypeError (env,NoOccurrenceFound op))
+      else if allow_K or dependent op t then
+	(evd,op::l)
       else
-	(evd,op::l))
+	(* This is not up to delta ... *)
+	raise (PretypeError (env,NoOccurrenceFound op)))
     oplist 
     (evd,[])
 
 let secondOrderAbstraction env allow_K typ (p, oplist) evd =
-  let sigma = evars_of (fst evd) in
+  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 (snd evd') p in
+  let typp = meta_type (metas_of 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 +443,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 (snd evd') ty1) ty2 evd'
+	w_unify_0 env cv_pb (nf_meta (metas_of 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 (snd evd') ty2) evd'
+	w_unify_0 env cv_pb ty1 (nf_meta (metas_of evd') ty2) evd'
     | _ -> error "w_unify2"
 
 
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 02d1918be..d3007e69d 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -18,19 +18,19 @@ open Evd
 open Evarutil
 (*i*)
 
-type maps = evar_defs * meta_map
-
-val w_Declare : env -> evar -> types -> maps -> maps
-val w_Define : evar -> constr -> maps -> maps
+val w_Declare : env -> evar -> types -> evar_defs -> evar_defs
+val w_Define : evar -> constr -> evar_defs -> evar_defs
 
 (* The "unique" unification fonction *)
 val w_unify :
-  bool -> env -> Reductionops.conv_pb -> constr -> constr -> maps -> maps
+  bool -> env -> Reductionops.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
    subterm of [t] is also returned. *)
-val w_unify_to_subterm : env -> constr * constr -> maps -> maps * constr
+val w_unify_to_subterm :
+  env -> constr * constr -> evar_defs -> evar_defs * constr
 
 (*i This should be in another module i*)