Raffinement de l'unification de "apply": mémorisation de certains

degrés de liberté concernant les instances de méta (cumulativité et
possibilité d'éta-expansion) de telle sorte que la fusion d'équations
se fasse modulo ces degrés de liberté.


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

8 files changed, 194 insertions, 52 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index a866da8264..d86f03e94e 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -156,7 +156,7 @@ let mentions clenv mv0 =
   let rec menrec mv1 =
     mv0 = mv1 ||
     let mlist =
-      try (meta_fvalue clenv.env mv1).freemetas
+      try (fst (meta_fvalue clenv.env mv1)).freemetas
       with Anomaly _ | Not_found -> Metaset.empty in
     meta_exists menrec mlist
   in menrec
@@ -180,11 +180,11 @@ let clenv_assign mv rhs clenv =
     error "clenv_assign: circularity in unification";
   try
     if meta_defined clenv.env mv then
-      if not (eq_constr (meta_fvalue clenv.env mv).rebus rhs) then
+      if not (eq_constr (fst (meta_fvalue clenv.env mv)).rebus rhs) then
         error_incompatible_inst clenv mv
       else
 	clenv
-    else {clenv with env = meta_assign mv rhs_fls.rebus clenv.env}
+    else {clenv with env = meta_assign mv (rhs_fls.rebus,ConvUpToEta 0) clenv.env}
   with Not_found -> 
     error "clenv_assign: undefined meta"
 
@@ -362,7 +362,7 @@ let clenv_match_args s clause =
     | (loc,b,c)::t ->
 	let k = meta_of_binder clause loc b t mvs in
         if meta_defined clause.env k then
-          if eq_constr (meta_fvalue clause.env k).rebus c then
+          if eq_constr (fst (meta_fvalue clause.env k)).rebus c then
             matchrec clause t
           else error_already_defined b
         else
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 5a353978d4..fb4321bc36 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -323,16 +323,24 @@ let mk_freelisted c =
 
 let map_fl f cfl = { cfl with rebus=f cfl.rebus }
 
+(* Status of an instance wrt to the meta it solves:
+  - a supertype of the meta (e.g. the solution to ?X <= T is a supertype of ?X)
+  - a subtype of the meta (e.g. the solution to T <= ?X is a supertype of ?X)
+  - a term that can be eta-expanded n times while still being a solution
+    (e.g. the solution [P] to [?X u v = P u v] can be eta-expanded twice)
+*)
+
+type instance_status = IsSuperType | IsSubType | ConvUpToEta of int
 
 (* Clausal environments *)
 
 type clbinding =
   | Cltyp of name * constr freelisted
-  | Clval of name * constr freelisted * constr freelisted
+  | Clval of name * (constr freelisted * instance_status) * constr freelisted
 
 let map_clb f = function
   | Cltyp (na,cfl) -> Cltyp (na,map_fl f cfl)
-  | Clval (na,cfl1,cfl2) -> Clval (na,map_fl f cfl1,map_fl f cfl2)
+  | Clval (na,(cfl1,pb),cfl2) -> Clval (na,(map_fl f cfl1,pb),map_fl f cfl2)
 
 (* name of defined is erased (but it is pretty-printed) *)
 let clb_name = function
@@ -469,12 +477,19 @@ let meta_ftype evd mv =
 let meta_declare mv v ?(name=Anonymous) evd =
   { evd with metas = Metamap.add mv (Cltyp(name,mk_freelisted v)) evd.metas }
   
-let meta_assign mv v evd =
+let meta_assign mv (v,pb) evd =
+  match Metamap.find mv evd.metas with
+  | Cltyp(na,ty) ->
+      { evd with
+        metas = Metamap.add mv (Clval(na,(mk_freelisted v,pb),ty)) evd.metas }
+  | _ -> anomaly "meta_assign: already defined"
+
+let meta_reassign mv (v,pb) evd =
   match Metamap.find mv evd.metas with
-      Cltyp(na,ty) ->
-        { evd with
-          metas = Metamap.add mv (Clval(na,mk_freelisted v, ty)) evd.metas }
-    | _ -> anomaly "meta_assign: already defined"
+  | Clval(na,_,ty) ->
+      { evd with
+        metas = Metamap.add mv (Clval(na,(mk_freelisted v,pb),ty)) evd.metas }
+  | _ -> anomaly "meta_reassign: not yet defined"
 
 (* If the meta is defined then forget its name *)
 let meta_name evd mv =
@@ -522,7 +537,7 @@ let pr_meta_map mmap =
       	hov 0 
 	  (pr_meta mv ++ pr_name na ++ str " : " ++
            print_constr b.rebus ++ fnl ())
-    | (mv,Clval(na,b,_)) ->
+    | (mv,Clval(na,(b,_),_)) ->
       	hov 0 
 	  (pr_meta mv ++ pr_name na ++ str " := " ++
            print_constr b.rebus ++ fnl ())
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 601c6c8b03..b4aa5fa5e0 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -99,9 +99,18 @@ val metavars_of : constr -> Metaset.t
 val mk_freelisted : constr -> constr freelisted
 val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted
 
+(* Status of an instance wrt to the meta it solves:
+  - a supertype of the meta (e.g. the solution to ?X <= T is a supertype of ?X)
+  - a subtype of the meta (e.g. the solution to T <= ?X is a supertype of ?X)
+  - a term that can be eta-expanded n times while still being a solution
+    (e.g. the solution [P] to [?X u v = P u v] can be eta-expanded twice)
+*)
+
+type instance_status = IsSuperType | IsSubType | ConvUpToEta of int
+
 type clbinding =
   | Cltyp of name * constr freelisted
-  | Clval of name * constr freelisted * constr freelisted
+  | Clval of name * (constr freelisted * instance_status) * constr freelisted
 
 val map_clb : (constr -> constr) -> clbinding -> clbinding
 
@@ -146,13 +155,14 @@ val meta_list : evar_defs -> (metavariable * clbinding) list
 val meta_defined : evar_defs -> metavariable -> bool
 (* [meta_fvalue] raises [Not_found] if meta not in map or [Anomaly] if
    meta has no value *)  
-val meta_fvalue    : evar_defs -> metavariable -> constr freelisted
+val meta_fvalue    : evar_defs -> metavariable -> constr freelisted * instance_status
 val meta_ftype     : evar_defs -> metavariable -> constr freelisted
 val meta_name      : evar_defs -> metavariable -> name
 val meta_with_name : evar_defs -> identifier -> metavariable
 val meta_declare   :
   metavariable -> types -> ?name:name -> evar_defs -> evar_defs
-val meta_assign    : metavariable -> constr -> evar_defs -> evar_defs
+val meta_assign    : metavariable -> constr * instance_status -> evar_defs -> evar_defs
+val meta_reassign  : metavariable -> constr * instance_status -> evar_defs -> evar_defs
 
 (* [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *)
 val meta_merge : evar_defs -> evar_defs -> evar_defs
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 76a053872a..481fa16eea 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -862,7 +862,7 @@ let is_arity env sigma c =
 let meta_value evd mv = 
   let rec valrec mv =
     try
-      let b = meta_fvalue evd mv in
+      let b,_ = meta_fvalue evd mv in
       instance
         (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas))
         b.rebus
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 0f99d9f7aa..7843b2226e 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -49,10 +49,41 @@ let abstract_list_all env sigma typ c l =
 
 (**)
 
+(* A refinement of [conv_pb]: the integers tells how many arguments
+   were applied in the context of the conversion problem; if the number
+   is non zero, steps of eta-expansion will be allowed
+*)
+
+type conv_pb_up_to_eta = Cumul | ConvUnderApp of int * int
+
+let topconv = ConvUnderApp (0,0)
+let of_conv_pb = function CONV -> topconv | CUMUL -> Cumul
+let conv_pb_of = function ConvUnderApp _ -> CONV | Cumul -> CUMUL
+let prod_pb = function ConvUnderApp _ -> topconv | pb -> pb
+
+let opp_status = function
+  | IsSuperType -> IsSubType
+  | IsSubType -> IsSuperType
+  | ConvUpToEta _ as x -> x
+
+let extract_instance_status = function
+  | Cumul -> (IsSubType,IsSuperType)
+  | ConvUnderApp (n1,n2) -> ConvUpToEta n1, ConvUpToEta n2
+
+let rec assoc_pair x = function
+    [] -> raise Not_found
+  | (a,b,_)::l -> if compare a x = 0 then b else assoc_pair x l
+
+let rec subst_meta_instances bl c =
+  match kind_of_term c with
+    | Meta i -> (try assoc_pair i bl with Not_found -> c)
+    | _ -> map_constr (subst_meta_instances bl) c
+
 let solve_pattern_eqn_array env f l c (metasubst,evarsubst) =
   match kind_of_term f with
     | Meta k -> 
-	(k,solve_pattern_eqn env (Array.to_list l) c)::metasubst,evarsubst
+	let pb = ConvUpToEta (Array.length l) in
+	(k,solve_pattern_eqn env (Array.to_list l) c,pb)::metasubst,evarsubst
     | Evar ev ->
       (* Currently unused: incompatible with eauto/eassumption backtracking *)
 	metasubst,(f,solve_pattern_eqn env (Array.to_list l) c)::evarsubst
@@ -81,7 +112,8 @@ let sort_eqns = unify_r2l
 let unify_0 env sigma cv_pb mod_delta m n =
   let trivial_unify pb substn m n =
     if (not(occur_meta m)) && 
-      (if mod_delta then is_fconv pb env sigma m n else eq_constr m n) 
+      (if mod_delta then is_fconv (conv_pb_of pb) env sigma m n
+       else eq_constr m n)
     then substn
     else error_cannot_unify env sigma (m,n) in
   let rec unirec_rec curenv pb ((metasubst,evarsubst) as substn) curm curn =
@@ -89,29 +121,31 @@ let unify_0 env sigma cv_pb mod_delta m n =
     and cN = Evarutil.whd_castappevar sigma curn in 
       match (kind_of_term cM,kind_of_term cN) with
 	| Meta k1, Meta k2 ->
+	    let stM,stN = extract_instance_status pb in
 	    if k1 < k2 
-	    then (k1,cN)::metasubst,evarsubst
-	    else if k1 = k2 then substn else (k2,cM)::metasubst,evarsubst
+	    then (k1,cN,stN)::metasubst,evarsubst
+	    else if k1 = k2 then substn
+	    else (k2,cM,stM)::metasubst,evarsubst
 	| Meta k, _    -> 
 	    (* Here we check that [cN] does not contain any local variables *)
 	    if (closedn (nb_rel env) cN)
-	    then (k,cN)::metasubst,evarsubst
+	    then (k,cN,snd (extract_instance_status pb))::metasubst,evarsubst
 	    else error_cannot_unify_local curenv sigma (curenv,m,n,cN)
 	| _, Meta k    -> 
 	    (* Here we check that [cM] does not contain any local variables *)
-	    if (closedn (nb_rel env) cM) 
-	    then (k,cM)::metasubst,evarsubst
+	    if (closedn (nb_rel env) cM)
+	    then (k,cM,fst (extract_instance_status pb))::metasubst,evarsubst
 	    else error_cannot_unify_local curenv sigma (curenv,m,n,cM)
 	| Evar _, _ -> metasubst,((cM,cN)::evarsubst)
 	| _, Evar _ -> metasubst,((cN,cM)::evarsubst)
 	| Lambda (na,t1,c1), Lambda (_,t2,c2) ->
-	    unirec_rec (push_rel_assum (na,t1) curenv) CONV 
-	      (unirec_rec curenv CONV substn t1 t2) c1 c2
+	    unirec_rec (push_rel_assum (na,t1) curenv) topconv
+	      (unirec_rec curenv topconv substn t1 t2) c1 c2
 	| Prod (na,t1,c1), Prod (_,t2,c2) ->
-	    unirec_rec (push_rel_assum (na,t1) curenv) pb 
-	      (unirec_rec curenv CONV substn t1 t2) c1 c2
-	| LetIn (_,b,_,c), _ -> unirec_rec curenv  pb substn (subst1 b c) cN
-	| _, LetIn (_,b,_,c) -> unirec_rec curenv  pb substn cM (subst1 b c)
+	    unirec_rec (push_rel_assum (na,t1) curenv) (prod_pb pb)
+	      (unirec_rec curenv topconv substn t1 t2) c1 c2
+	| LetIn (_,b,_,c), _ -> unirec_rec curenv pb substn (subst1 b c) cN
+	| _, LetIn (_,b,_,c) -> unirec_rec curenv pb substn cM (subst1 b c)
 	    
 	| App (f1,l1), App (f2,l2) ->
 	    if
@@ -133,25 +167,82 @@ let unify_0 env sigma cv_pb mod_delta m n =
 		else 
 		  let extras,restl1 = array_chop (len1-len2) l1 in 
 		    (appvect (f1,extras), restl1, f2, l2) in
+	      let pb = ConvUnderApp (len1,len2) in
 		(try
-		    array_fold_left2 (unirec_rec curenv CONV)
-		      (unirec_rec curenv CONV substn f1 f2) l1 l2
+		    array_fold_left2 (unirec_rec curenv topconv)
+		      (unirec_rec curenv pb substn f1 f2) l1 l2
 		  with ex when precatchable_exception ex ->
 		    trivial_unify pb substn cM cN)
 	| Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
-            array_fold_left2 (unirec_rec curenv CONV)
-	      (unirec_rec curenv CONV 
-		  (unirec_rec curenv CONV substn p1 p2) c1 c2) cl1 cl2
+            array_fold_left2 (unirec_rec curenv topconv)
+	      (unirec_rec curenv topconv
+		  (unirec_rec curenv topconv substn p1 p2) c1 c2) cl1 cl2
 	| _ -> trivial_unify pb substn cM cN
   in
     if (not(occur_meta m)) &&
-      (if mod_delta then is_fconv cv_pb env sigma m n else eq_constr m n)
+      (if mod_delta then is_fconv (conv_pb_of cv_pb) env sigma m n
+       else eq_constr m n)
     then 
       ([],[])
     else 
       let (mc,ec) = unirec_rec env cv_pb ([],[]) m n in
 	((*sort_eqns*) mc, (*sort_eqns*) ec)
 
+let left = true
+let right = false
+
+let pop k = if k=0 then 0 else k-1
+
+let rec unify_with_eta keptside mod_delta env sigma k1 k2 c1 c2 =
+  (* Reason up to limited eta-expansion: ci is allowed to start with ki lam *)
+  (* Question: try whd_betadeltaiota on ci if ki>0 ? *)
+  match kind_of_term c1, kind_of_term c2 with
+  | (Lambda (na,t1,c1'), Lambda (_,t2,c2')) ->
+      let env' = push_rel_assum (na,t1) env in
+      let metas,evars = unify_0 env sigma topconv mod_delta t1 t2 in
+      let side,status,(metas',evars') =
+	unify_with_eta keptside mod_delta env' sigma (pop k1) (pop k2) c1' c2'
+      in (side,status,(metas@metas',evars@evars'))
+  | (Lambda (na,t,c1'),_) when k2 > 0 ->
+      let env' = push_rel_assum (na,t) env in
+      let side = left in (* expansion on the right: we keep the left side *)
+      unify_with_eta side mod_delta env' sigma (pop k1) (k2-1) 
+	c1' (mkApp (lift 1 c2,[|mkRel 1|]))
+  | (_,Lambda (na,t,c2')) when k1 > 0 ->
+      let env' = push_rel_assum (na,t) env in
+      let side = right in (* expansion on the left: we keep the right side *)
+      unify_with_eta side mod_delta env' sigma (k1-1) (pop k2) 
+	(mkApp (lift 1 c1,[|mkRel 1|])) c2'
+  | _ ->
+      (keptside,ConvUpToEta(min k1 k2),
+       unify_0 env sigma topconv mod_delta c1 c2)
+
+(* We solved problems [?n =_pb u] (i.e. [u =_(opp pb) ?n]) and [?n =_pb' u'],
+   we now compute the problem on [u =? u'] and decide which of u or u' is kept
+
+   Rem: the upper constraint is lost in case u <= ?n <= u' (and symmetrically
+   in the case u' <= ?n <= u)
+ *)
+
+let merge_instances env sigma mod_delta st1 st2 c1 c2 =
+  match (opp_status st1, st2) with
+  | (ConvUpToEta n1, ConvUpToEta n2) ->
+      let side = left (* arbitrary choice, but agrees with compatibility *) in
+      unify_with_eta side mod_delta env sigma n1 n2 c1 c2
+  | ((IsSubType  |ConvUpToEta _ as oppst1),(IsSubType  |ConvUpToEta _)) ->
+      let res = unify_0 env sigma Cumul mod_delta c2 c1 in
+      if oppst1=st2 then (* arbitrary choice *) (left, st1, res)
+      else (st2=IsSubType, ConvUpToEta 0, res)
+  | ((IsSuperType|ConvUpToEta _ as oppst1),(IsSuperType|ConvUpToEta _)) ->
+      let res = unify_0 env sigma Cumul mod_delta c1 c2 in
+      if oppst1=st2 then (* arbitrary choice *) (left, st1, res)
+      else (st2=IsSuperType, ConvUpToEta 0, res)
+  | (IsSuperType,IsSubType) ->
+      (try (left, IsSubType, unify_0 env sigma Cumul mod_delta c2 c1)
+       with _ -> (right, IsSubType, unify_0 env sigma Cumul mod_delta c1 c2))
+  | (IsSubType,IsSuperType) ->
+      (try (left, IsSuperType, unify_0 env sigma Cumul mod_delta c1 c2)
+       with _ -> (right, IsSuperType, unify_0 env sigma Cumul mod_delta c2 c1))
 
 (* Unification
  *
@@ -234,7 +325,7 @@ let w_merge env with_types mod_delta metas evars evd =
       | ((lhs,rhs)::t, metas) ->
       (match kind_of_term rhs with
 
-	| Meta k -> w_merge_rec evd ((k,lhs)::metas) t
+	| Meta k -> w_merge_rec evd ((k,lhs,ConvUpToEta 0)::metas) t
 
 	| krhs ->
         (match kind_of_term lhs with
@@ -242,11 +333,12 @@ let w_merge env with_types mod_delta metas evars evd =
 	  | Evar (evn,_ as ev) ->
     	      if is_defined_evar evd ev then
 		let (metas',evars') =
-                  unify_0 env (evars_of evd) CONV mod_delta rhs lhs in
+                  unify_0 env (evars_of evd) topconv mod_delta rhs lhs in
 		w_merge_rec evd (metas'@metas) (evars'@t)
     	      else begin
-		let rhs' = 
-		  if occur_meta rhs then subst_meta metas rhs else rhs 
+		let rhs' =
+		  if occur_meta rhs then subst_meta_instances metas rhs
+		  else rhs 
 		in
 		if occur_evar evn rhs' then
                   error "w_merge: recursive equation";
@@ -265,12 +357,16 @@ let w_merge env with_types mod_delta metas evars evd =
 
 	  | _ -> anomaly "w_merge_rec"))
 
-      | ([], (mv,n)::t) ->
+      | ([], (mv,n,status)::t) ->
     	  if meta_defined evd mv then
-            let (metas',evars') =
-              unify_0 env (evars_of evd) CONV mod_delta
-               (meta_fvalue evd mv).rebus n in
-            w_merge_rec evd (metas'@t) evars'
+	    let n',status' = meta_fvalue evd mv in
+	    let n' = n'.rebus in
+            let (take_left,st,(metas',evars')) =
+	      merge_instances env (evars_of evd) mod_delta status' status n' n
+	    in
+	    let evd' = if take_left then evd else meta_reassign mv (n,st) evd 
+	    in
+            w_merge_rec evd' (metas'@t) evars'
     	  else
             begin
 	      if with_types (* or occur_meta mvty *) then
@@ -279,11 +375,11 @@ let w_merge env with_types mod_delta metas evars evd =
                   let sigma = evars_of evd in
                   (* why not typing with the metamap ? *)
 		  let nty = Typing.type_of env sigma (nf_meta evd n) in
-		  let (mc,ec) = unify_0 env sigma CUMUL mod_delta nty mvty in
+		  let (mc,ec) = unify_0 env sigma Cumul mod_delta nty mvty in
                   ty_metas := mc @ !ty_metas;
                   ty_evars := ec @ !ty_evars
 		with e when precatchable_exception e -> ());
-              let evd' = meta_assign mv n evd in
+              let evd' = meta_assign mv (n,status) evd in
 	      w_merge_rec evd' t []
             end
 
@@ -292,7 +388,7 @@ let w_merge env with_types mod_delta metas evars evd =
     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 mod_delta
+      unify_0 sp_env (evars_of evd') Cumul mod_delta
         (Retyping.get_type_of sp_env (evars_of evd') c) ev.evar_concl in
     let evd'' = w_merge_rec evd' mc ec in
     if (evars_of evd') == (evars_of evd'')
@@ -347,7 +443,7 @@ let w_unify_to_subterm env ?(mod_delta=true) (op,cl) evd =
     let cl = strip_outer_cast cl in
     (try 
        if closed0 cl 
-       then w_unify_0 env CONV mod_delta op cl evd,cl
+       then w_unify_0 env topconv mod_delta op cl evd,cl
        else error "Bound 1"
      with ex when precatchable_exception ex ->
        (match kind_of_term cl with 
@@ -427,7 +523,7 @@ let secondOrderAbstraction env mod_delta allow_K typ (p, oplist) evd =
     w_unify_to_subterm_list env mod_delta allow_K oplist typ evd in
   let typp = Typing.meta_type evd' p in
   let pred = abstract_list_all env sigma typp typ cllist in
-  w_unify_0 env CONV mod_delta (mkMeta p) pred evd'
+  w_unify_0 env topconv mod_delta (mkMeta p) pred evd'
 
 let w_unify2 env mod_delta allow_K cv_pb ty1 ty2 evd =
   let c1, oplist1 = whd_stack ty1 in
@@ -469,6 +565,7 @@ let w_unify2 env mod_delta allow_K cv_pb ty1 ty2 evd =
    convertible and first-order otherwise. But if failed if e.g. the type of
    Meta(1) had meta-variables in it. *)
 let w_unify allow_K env cv_pb ?(mod_delta=true) ty1 ty2 evd =
+  let cv_pb = of_conv_pb cv_pb in
   let hd1,l1 = whd_stack ty1 in
   let hd2,l2 = whd_stack ty2 in
     match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index e7acd6d646..2e3e0d3c89 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -326,7 +326,7 @@ let enstack_subsubgoals env se stack gls=
 	    let (nlast,holes,nmetas) = 
 		meta_aux se.se_last_meta [] (List.rev rc) in
 	    let refiner = applist (appterm,List.rev holes) in
-	    let evd = meta_assign se.se_meta refiner se.se_evd in
+	    let evd = meta_assign se.se_meta (refiner,ConvUpToEta 0) se.se_evd in
 	    let ncreated = replace_in_list 
 	      se.se_meta nmetas se.se_meta_list in
 	    let evd0 = List.fold_left 
@@ -361,7 +361,7 @@ let find_subsubgoal env c ctyp skip evd metas gls =
 	  Unification.w_unify true env Reduction.CUMUL 
 	    ctyp se.se_type se.se_evd in
 	  if n <= 0 then 
-	      {se with se_evd=meta_assign se.se_meta c unifier}	  
+	      {se with se_evd=meta_assign se.se_meta (c,ConvUpToEta 0) unifier}
 	  else
 	      dfs (pred n)
       with _ -> 
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index f0dca6b2d1..5da0bb047a 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1729,7 +1729,7 @@ let check_evar_map_of_evars_defs evd =
      match binding with
         Evd.Cltyp (_,{Evd.rebus=rebus; Evd.freemetas=freemetas}) ->
          check_freemetas_is_empty rebus freemetas
-      | Evd.Clval (_,{Evd.rebus=rebus1; Evd.freemetas=freemetas1},
+      | Evd.Clval (_,({Evd.rebus=rebus1; Evd.freemetas=freemetas1},_),
                  {Evd.rebus=rebus2; Evd.freemetas=freemetas2}) ->
          check_freemetas_is_empty rebus1 freemetas1 ;
          check_freemetas_is_empty rebus2 freemetas2
diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v
index 6886962156..7acbb7d05e 100644
--- a/test-suite/success/unification.v
+++ b/test-suite/success/unification.v
@@ -63,3 +63,23 @@ Proof.
 intros.
 apply H.
 Qed.
+
+
+(* Test unification modulo eta-expansion (if possible) *)
+
+(* In this example, two instances for ?P (argument of hypothesis H) can be 
+   inferred (one is by unifying the type [Q true] and [?P true] of the
+   goal and type of [H]; the other is by unifying the argument of [f]);
+   we need to unify both instances up to allowed eta-expansions of the 
+   instances (eta is allowed if the meta was applied to arguments)
+
+   This used to fail before revision 9389 in trunk
+*)
+
+Lemma l4 :
+   forall f : (forall P, P true), (forall P, f P = f P) ->
+   forall Q, f (fun x => Q x) = f (fun x => Q x).
+Proof.
+intros.
+apply H.
+Qed.