Mise en place d'une toute petite amélioration de l'unification de

apply : si on a trouvé une méta, alors, on l'utilise pour instancier
les trous lors de la tentative de conversion modulo delta. Cela permet
ainsi de résoudre de petits cas d'unification, tel que celui annoncé
échouant dans le "beginner question" du 6 fevrier 2008 de coq-club.

Solde au passage de modifs cosmétiques de setoid_replace.ml avant
abandon probable du code.



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

7 files changed, 111 insertions, 88 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index b9881aaf04..18a22e5c71 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -241,18 +241,19 @@ let clenv_missing ce = clenv_dependent true ce
 
 (******************************************************************)
 
-let clenv_unify allow_K cv_pb t1 t2 clenv =
-  { clenv with evd = w_unify allow_K clenv.env cv_pb t1 t2 clenv.evd }
+let clenv_unify allow_K ?(flags=default_unify_flags) cv_pb t1 t2 clenv =
+  { clenv with
+      evd = w_unify allow_K ~flags:flags clenv.env cv_pb t1 t2 clenv.evd }
 
-let clenv_unify_meta_types clenv =
-  { clenv with evd = w_unify_meta_types clenv.env clenv.evd }
+let clenv_unify_meta_types ?(flags=default_unify_flags) clenv =
+  { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
 
-let clenv_unique_resolver allow_K clenv gl =
+let clenv_unique_resolver allow_K ?(flags=default_unify_flags) clenv gl =
   if isMeta (fst (whd_stack clenv.templtyp.rebus)) then
-    clenv_unify allow_K CUMUL (clenv_type clenv) (pf_concl gl)
-      (clenv_unify_meta_types clenv)
+    clenv_unify allow_K CUMUL ~flags:flags (clenv_type clenv) (pf_concl gl)
+      (clenv_unify_meta_types ~flags:flags clenv)
   else
-    clenv_unify allow_K CUMUL 
+    clenv_unify allow_K CUMUL ~flags:flags
       (meta_reducible_instance clenv.evd clenv.templtyp) (pf_concl gl) clenv
 
 (* [clenv_pose_dependent_evars clenv]
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index 8546a44ef3..e6cd960b20 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -18,6 +18,7 @@ open Evd
 open Evarutil
 open Mod_subst
 open Rawterm
+open Unification
 (*i*)
 
 (***************************************************************)
@@ -69,16 +70,16 @@ val clenv_fchain :
 
 (* Unifies two terms in a clenv. The boolean is [allow_K] (see [Unification]) *)
 val clenv_unify : 
-  bool -> conv_pb -> constr -> constr -> clausenv -> clausenv
+  bool -> ?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv
 
 (* unifies the concl of the goal with the type of the clenv *)
 val clenv_unique_resolver :
-  bool -> clausenv -> evar_info sigma -> clausenv
+  bool -> ?flags:unify_flags -> clausenv -> evar_info sigma -> clausenv
 
 (* same as above ([allow_K=false]) but replaces remaining metas
    with fresh evars if [evars_flag] is [true] *)
 val evar_clenv_unique_resolver :
-  bool -> clausenv -> evar_info sigma -> clausenv
+  bool -> ?flags:unify_flags -> clausenv -> evar_info sigma -> clausenv
 
 val clenv_pose_dependent_evars : clausenv -> clausenv
 
@@ -98,7 +99,7 @@ val clenv_constrain_last_binding : constr -> clausenv -> clausenv
 (* defines metas corresponding to the name of the bindings *)
 val clenv_match_args : arg_bindings -> clausenv -> clausenv
 
-val clenv_unify_meta_types : clausenv -> clausenv
+val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv
 
 (* start with a clenv to refine with a given term with bindings *)
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index b2190c53cf..cac80301f8 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -114,12 +114,17 @@ let unify_r2l x = x
 let sort_eqns = unify_r2l
 *)
 
-let unify_0_with_initial_metas metas env sigma cv_pb mod_delta m n =
+type unify_flags = { modulo_delta : bool; use_metas_eagerly : bool }
+
+let default_unify_flags = { modulo_delta = true; use_metas_eagerly = true }
+
+let unify_0_with_initial_metas metas env sigma cv_pb flags m n =
   let nb = nb_rel env in
   let trivial_unify pb (metasubst,_ as substn) m n =
-    match subst_defined_metas (* too strong: metasubst *) metas m with
+    let metas = if flags.use_metas_eagerly then metasubst else metas in
+    match subst_defined_metas metas m with
       | Some m when
-	  (if mod_delta then is_fconv (conv_pb_of pb) env sigma m n
+	  (if flags.modulo_delta then is_fconv (conv_pb_of pb) env sigma m n
 	  else eq_constr m n) -> substn
       | _ -> error_cannot_unify env sigma (m,n) in
   let rec unirec_rec curenv pb ((metasubst,evarsubst) as substn) curm curn =
@@ -185,7 +190,7 @@ let unify_0_with_initial_metas metas env sigma cv_pb mod_delta m n =
 	| _ -> trivial_unify pb substn cM cN
   in
     if (not(occur_meta m)) &&
-      (if mod_delta then is_fconv (conv_pb_of cv_pb) env sigma m n
+      (if flags.modulo_delta then is_fconv (conv_pb_of cv_pb) env sigma m n
        else eq_constr m n)
     then 
       (metas,[])
@@ -200,29 +205,29 @@ 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 =
+let rec unify_with_eta keptside flags 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 metas,evars = unify_0 env sigma topconv flags t1 t2 in
       let side,status,(metas',evars') =
-	unify_with_eta keptside mod_delta env' sigma (pop k1) (pop k2) c1' c2'
+	unify_with_eta keptside flags 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) 
+      unify_with_eta side flags 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) 
+      unify_with_eta side flags 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)
+       unify_0 env sigma topconv flags 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
@@ -231,33 +236,33 @@ let rec unify_with_eta keptside mod_delta env sigma k1 k2 c1 c2 =
    in the case u' <= ?n <= u)
  *)
 
-let merge_instances env sigma mod_delta st1 st2 c1 c2 =
+let merge_instances env sigma flags st1 st2 c1 c2 =
   match (opp_status st1, st2) with
   | (UserGiven, ConvUpToEta n2) ->
-      unify_with_eta left mod_delta env sigma 0 n2 c1 c2
+      unify_with_eta left flags env sigma 0 n2 c1 c2
   | (ConvUpToEta n1, UserGiven) ->
-      unify_with_eta right mod_delta env sigma n1 0 c1 c2
+      unify_with_eta right flags env sigma n1 0 c1 c2
   | (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
+      unify_with_eta side flags env sigma n1 n2 c1 c2
   | ((IsSubType | ConvUpToEta _ | UserGiven as oppst1),
      (IsSubType | ConvUpToEta _ | UserGiven)) ->
-      let res = unify_0 env sigma Cumul mod_delta c2 c1 in
+      let res = unify_0 env sigma Cumul flags c2 c1 in
       if oppst1=st2 then (* arbitrary choice *) (left, st1, res)
       else if st2=IsSubType or st1=UserGiven then (left, st1, res)
       else (right, st2, res)
   | ((IsSuperType | ConvUpToEta _ | UserGiven as oppst1),
      (IsSuperType | ConvUpToEta _ | UserGiven)) ->
-      let res = unify_0 env sigma Cumul mod_delta c1 c2 in
+      let res = unify_0 env sigma Cumul flags c1 c2 in
       if oppst1=st2 then (* arbitrary choice *) (left, st1, res)
       else if st2=IsSuperType or st1=UserGiven then (left, st1, res)
       else (right, st2, 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))
+      (try (left, IsSubType, unify_0 env sigma Cumul flags c2 c1)
+       with _ -> (right, IsSubType, unify_0 env sigma Cumul flags 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))
+      (try (left, IsSuperType, unify_0 env sigma Cumul flags c1 c2)
+       with _ -> (right, IsSuperType, unify_0 env sigma Cumul flags c2 c1))
 
 (* Unification
  *
@@ -336,13 +341,13 @@ let w_coerce env c ctyp target evd =
   with e when precatchable_exception e ->
     evd,c
 
-let unify_to_type env evd mod_delta c u =
+let unify_to_type env evd flags c u =
   let sigma = evars_of evd in
   let c = refresh_universes c in
   let t = get_type_of_with_meta env sigma (metas_of evd) c in
   let t = Tacred.hnf_constr env sigma (nf_betaiota (nf_meta evd t)) in
   let u = Tacred.hnf_constr env sigma u in
-  try unify_0 env sigma Cumul mod_delta t u
+  try unify_0 env sigma Cumul flags t u
   with e when precatchable_exception e -> ([],[])
 
 let coerce_to_type env evd c u =
@@ -350,19 +355,19 @@ let coerce_to_type env evd c u =
   let t = get_type_of_with_meta env (evars_of evd) (metas_of evd) c in
   w_coerce env c t u evd
 
-let unify_or_coerce_type env evd mod_delta mv c =
+let unify_or_coerce_type env evd flags mv c =
   let mvty = Typing.meta_type evd mv in
   (* nf_betaiota was before in type_of - useful to reduce
      types like (x:A)([x]P u) *)
   if occur_meta mvty then
-    (evd,c),unify_to_type env evd mod_delta c mvty
+    (evd,c),unify_to_type env evd flags c mvty
   else
     coerce_to_type env evd c mvty,([],[])
 
-let unify_type env evd mod_delta mv c =
+let unify_type env evd flags mv c =
   let mvty = Typing.meta_type evd mv in
   if occur_meta mvty then
-    unify_to_type env evd mod_delta c mvty
+    unify_to_type env evd flags c mvty
   else ([],[])
 
 (* Move metas that may need coercion at the end of the list of instances *)
@@ -379,7 +384,7 @@ let order_metas metas =
    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 mod_delta metas evars evd =
+let w_merge env with_types flags metas evars evd =
   let rec w_merge_rec evd metas evars eqns =
 
     (* Process evars *)
@@ -388,7 +393,7 @@ let w_merge env with_types mod_delta metas evars evd =
     	if is_defined_evar evd ev then
 	  let v = Evd.existential_value (evars_of evd) ev in
 	  let (metas',evars'') =
-	    unify_0 env (evars_of evd) topconv mod_delta rhs v in
+	    unify_0 env (evars_of evd) topconv flags rhs v in
 	  w_merge_rec evd (metas'@metas) (evars''@evars') eqns
     	else begin
           let rhs' = subst_meta_instances metas rhs in
@@ -400,7 +405,7 @@ let w_merge env with_types mod_delta metas evars evd =
                     metas evars' eqns
 		with ex when precatchable_exception ex ->
                   let evd' =
-                    mimick_evar evd mod_delta f (Array.length cl) evn in
+                    mimick_evar evd flags f (Array.length cl) evn in
 		  w_merge_rec evd' metas evars eqns)
           | _ ->
               (* ensure tail recursion in non-mimickable case! *)
@@ -415,7 +420,7 @@ let w_merge env with_types mod_delta metas evars evd =
 	  if with_types & to_type <> TypeProcessed then
 	    if to_type = CoerceToType then
               (* Some coercion may have to be inserted *)
-	      (unify_or_coerce_type env evd mod_delta mv c,[])
+	      (unify_or_coerce_type env evd flags mv c,[])
 	    else
               (* No coercion needed: delay the unification of types *)
 	      ((evd,c),([],[])),(mv,c)::eqns
@@ -424,7 +429,7 @@ let w_merge env with_types mod_delta metas evars evd =
     	if meta_defined evd mv then
 	  let {rebus=c'},(status',_) = meta_fvalue evd mv in
           let (take_left,st,(metas',evars')) =
-	    merge_instances env (evars_of evd) mod_delta status' status c' c
+	    merge_instances env (evars_of evd) flags status' status c' c
 	  in
 	  let evd' = 
             if take_left then evd 
@@ -439,16 +444,16 @@ let w_merge env with_types mod_delta metas evars evd =
     (* Process type eqns *)
     match eqns with
     | (mv,c)::eqns ->
-        let (metas,evars) = unify_type env evd mod_delta mv c in 
+        let (metas,evars) = unify_type env evd flags mv c in 
         w_merge_rec evd metas evars eqns
     | [] -> evd
 		
-  and mimick_evar evd mod_delta hdc nargs sp =
+  and mimick_evar evd flags hdc nargs sp =
     let ev = Evd.find (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 mod_delta
+      unify_0 sp_env (evars_of evd') Cumul flags
         (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'')
@@ -458,9 +463,9 @@ let w_merge env with_types mod_delta metas evars evd =
   (* merge constraints *)
   w_merge_rec evd (order_metas metas) evars []
 
-let w_unify_meta_types env evd =
+let w_unify_meta_types env ?(flags=default_unify_flags) evd =
   let metas,evd = retract_coercible_metas evd in
-  w_merge env true true metas [] evd
+  w_merge env true flags metas [] evd
 
 (* [w_unify env evd M N]
    performs a unification of M and N, generating a bunch of
@@ -472,11 +477,12 @@ let w_unify_meta_types env evd =
    [clenv_typed_unify M N clenv] expects in addition that expected
    types of metavars are unifiable with the types of their instances    *)
 
-let w_unify_core_0 env with_types cv_pb mod_delta m n evd =
+let w_unify_core_0 env with_types cv_pb flags m n evd =
   let (mc1,evd') = retract_coercible_metas evd in
   let (mc2,ec) = 
-    unify_0_with_initial_metas mc1 env (evars_of evd') cv_pb mod_delta m n in 
-  w_merge env with_types mod_delta mc2 ec evd'
+    unify_0_with_initial_metas mc1 env (evars_of evd') cv_pb flags m n
+  in 
+  w_merge env with_types flags mc2 ec evd'
 
 let w_unify_0 env = w_unify_core_0 env false
 let w_typed_unify env = w_unify_core_0 env true
@@ -498,12 +504,12 @@ let iter_fail f a =
 (* Tries to find an instance of term [cl] in term [op].
    Unifies [cl] to every subterm of [op] until it finds a match.
    Fails if no match is found *)
-let w_unify_to_subterm env ?(mod_delta=true) (op,cl) evd =
+let w_unify_to_subterm env ?(flags=default_unify_flags) (op,cl) evd =
   let rec matchrec cl =
     let cl = strip_outer_cast cl in
     (try 
        if closed0 cl 
-       then w_unify_0 env topconv mod_delta op cl evd,cl
+       then w_unify_0 env topconv flags op cl evd,cl
        else error "Bound 1"
      with ex when precatchable_exception ex ->
        (match kind_of_term cl with 
@@ -555,7 +561,7 @@ let w_unify_to_subterm env ?(mod_delta=true) (op,cl) evd =
   with ex when precatchable_exception ex ->
     raise (PretypeError (env,NoOccurrenceFound op))
 
-let w_unify_to_subterm_list env mod_delta allow_K oplist t evd = 
+let w_unify_to_subterm_list env flags allow_K oplist t evd = 
   List.fold_right 
     (fun op (evd,l) ->
       if isMeta op then
@@ -565,7 +571,7 @@ let w_unify_to_subterm_list env mod_delta allow_K oplist t evd =
         let (evd',cl) =
           try 
 	    (* This is up to delta for subterms w/o metas ... *)
-	    w_unify_to_subterm env ~mod_delta (strip_outer_cast op,t) evd
+	    w_unify_to_subterm env ~flags (strip_outer_cast op,t) evd
           with PretypeError (env,NoOccurrenceFound _) when allow_K -> (evd,op)
         in 
 	(evd',cl::l)
@@ -577,29 +583,29 @@ let w_unify_to_subterm_list env mod_delta allow_K oplist t evd =
     oplist 
     (evd,[])
 
-let secondOrderAbstraction env mod_delta allow_K typ (p, oplist) evd =
+let secondOrderAbstraction env flags allow_K typ (p, oplist) evd =
   let (evd',cllist) =
-    w_unify_to_subterm_list env mod_delta allow_K oplist typ evd in
+    w_unify_to_subterm_list env flags allow_K oplist typ evd in
   let typp = Typing.meta_type evd' p in
   let pred = abstract_list_all env evd' typp typ cllist in
-  w_unify_0 env topconv mod_delta (mkMeta p) pred evd'
+  w_unify_0 env topconv flags (mkMeta p) pred evd'
 
-let w_unify2 env mod_delta allow_K cv_pb ty1 ty2 evd =
+let w_unify2 env flags allow_K cv_pb ty1 ty2 evd =
   let c1, oplist1 = whd_stack ty1 in
   let c2, oplist2 = whd_stack ty2 in
   match kind_of_term c1, kind_of_term c2 with
     | Meta p1, _ ->
         (* Find the predicate *)
 	let evd' =
-          secondOrderAbstraction env mod_delta allow_K ty2 (p1,oplist1) evd in 
+          secondOrderAbstraction env flags allow_K ty2 (p1,oplist1) evd in 
         (* Resume first order unification *)
-	w_unify_0 env cv_pb mod_delta (nf_meta evd' ty1) ty2 evd'
+	w_unify_0 env cv_pb flags (nf_meta evd' ty1) ty2 evd'
     | _, Meta p2 ->
         (* Find the predicate *)
 	let evd' =
-          secondOrderAbstraction env mod_delta allow_K ty1 (p2, oplist2) evd in 
+          secondOrderAbstraction env flags allow_K ty1 (p2, oplist2) evd in 
         (* Resume first order unification *)
-	w_unify_0 env cv_pb mod_delta ty1 (nf_meta evd' ty2) evd'
+	w_unify_0 env cv_pb flags ty1 (nf_meta evd' ty2) evd'
     | _ -> error "w_unify2"
 
 
@@ -623,7 +629,7 @@ let w_unify2 env mod_delta allow_K cv_pb ty1 ty2 evd =
    Before, second-order was used if the type of Meta(1) and [x:A]t was
    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 w_unify allow_K env cv_pb ?(flags=default_unify_flags) 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
@@ -632,10 +638,10 @@ let w_unify allow_K env cv_pb ?(mod_delta=true) ty1 ty2 evd =
       | (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true)
 	  when List.length l1 = List.length l2 ->
 	  (try 
-	      w_typed_unify env cv_pb mod_delta ty1 ty2 evd
+	      w_typed_unify env cv_pb flags ty1 ty2 evd
 	    with ex when precatchable_exception ex -> 
 	      try 
-		w_unify2 env mod_delta allow_K cv_pb ty1 ty2 evd
+		w_unify2 env flags allow_K cv_pb ty1 ty2 evd
 	      with PretypeError (env,NoOccurrenceFound c) as e -> raise e
 		| ex when precatchable_exception ex -> 
 		    error "Cannot solve a second-order unification problem")
@@ -643,14 +649,14 @@ let w_unify allow_K env cv_pb ?(mod_delta=true) ty1 ty2 evd =
       (* Second order case *)
       | (Meta _, true, _, _ | _, _, Meta _, true) -> 
 	  (try 
-	      w_unify2 env mod_delta allow_K cv_pb ty1 ty2 evd
+	      w_unify2 env flags allow_K cv_pb ty1 ty2 evd
 	    with PretypeError (env,NoOccurrenceFound c) as e -> raise e
 	      | ex when precatchable_exception ex -> 
 		  try 
-		    w_typed_unify env cv_pb mod_delta ty1 ty2 evd
+		    w_typed_unify env cv_pb flags ty1 ty2 evd
 		  with ex when precatchable_exception ex -> 
 		    error "Cannot solve a second-order unification problem")
 	    
       (* General case: try first order *)
-      | _ -> w_typed_unify env cv_pb mod_delta ty1 ty2 evd
+      | _ -> w_typed_unify env cv_pb flags ty1 ty2 evd
 
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index d2cb20550b..f0717b2a70 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -14,17 +14,21 @@ open Environ
 open Evd
 (*i*)
 
+type unify_flags = { modulo_delta : bool; use_metas_eagerly : bool }
+
+val default_unify_flags : unify_flags
+
 (* The "unique" unification fonction *)
 val w_unify :
-  bool -> env -> conv_pb -> ?mod_delta:bool -> constr -> constr -> evar_defs -> evar_defs
+  bool -> env -> conv_pb -> ?flags:unify_flags -> 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 -> ?mod_delta:bool -> constr * constr -> evar_defs -> evar_defs * constr
+  env -> ?flags:unify_flags -> constr * constr -> evar_defs -> evar_defs * constr
 
-val w_unify_meta_types : env -> evar_defs -> evar_defs
+val w_unify_meta_types : env -> ?flags:unify_flags -> evar_defs -> evar_defs
 
 (*i This should be in another module i*)
 
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 480ca95609..ebba4b00bb 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -556,12 +556,18 @@ let print_searchtable () =
 
 let priority l = List.map snd (List.filter (fun (pr,_) -> pr = 0) l)
 
+(* tell auto not to reuse already instantiated metas in unification (for
+   compatibility, since otherwise, apply succeeds oftener) *)
+
+open Unification
+
+let auto_unif_flags = { modulo_delta = true; use_metas_eagerly = false }
 
 (* Try unification with the precompiled clause, then use registered Apply *)
 
 let unify_resolve (c,clenv) gls = 
   let clenv' = connect_clenv gls clenv in
-  let _ = clenv_unique_resolver false clenv' gls in  
+  let _ = clenv_unique_resolver false ~flags:auto_unif_flags clenv' gls in  
   h_simplest_apply c gls
 
 (* builds a hint database from a constr signature *)
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 477beba4ab..fb25d9d25d 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -210,7 +210,9 @@ let coq_impl = lazy(constant ["Setoid_tac"] "impl")
 (************************* Table of declared relations **********************)
 
 
-(* Relations are stored in a table which is synchronised with the Reset mechanism. *)
+(* Relations are stored in a table which is synchronised with the
+   Reset mechanism. The table maps the term denoting the relation to
+   the data of type relation that characterises the relation *)
 
 let relation_table = ref Gmap.empty
 
@@ -1464,12 +1466,9 @@ let mark_occur gl ~new_goals t in_c input_relation input_direction =
                           (MApp (func,mor,a,output_direction)))
 			  output_directions @ res
                     ) [] a'
-              | (he::tl) as a->
+              | (he::tl) ->
                  let typnf = Reduction.whd_betadeltaiota env typ in
                   match kind_of_term typnf with
-                    Cast (typ,_,_) ->
-                     find_non_dependent_function env c c_args_rev typ
-                      f_args_rev a_rev a
                   | Prod (name,s,t) ->
                      let env' = push_rel (name,None,s) env in
                      let he =
@@ -1564,12 +1563,12 @@ let mark_occur gl ~new_goals t in_c input_relation input_direction =
   match res' with
      [] when res = [] ->
       errorlabstrm "Setoid_rewrite"
-       (str "Either the term " ++ pr_lconstr t ++ str " that must be " ++
-        str "rewritten occurs in a covariant position or the goal is not " ++
-        str "made of morphism applications only. You can replace only " ++
-        str "occurrences that are in a contravariant position and such that " ++
-        str "the context obtained by abstracting them is made of morphism " ++
-        str "applications only.")
+       (strbrk "Either the term " ++ pr_lconstr t ++ strbrk " that must be " ++
+        strbrk "rewritten occurs in a covariant position or the goal is not" ++
+        strbrk " made of morphism applications only. You can replace only " ++
+        strbrk "occurrences that are in a contravariant position and such " ++
+        strbrk "that the context obtained by abstracting them is made of " ++
+        strbrk "morphism applications only.")
    | [] ->
       errorlabstrm "Setoid_rewrite"
        (str "No generated set of side conditions is a superset of those " ++
@@ -1732,18 +1731,22 @@ let check_evar_map_of_evars_defs evd =
 (* [unification_rewrite] searchs a match for [c1] in [but] and then 
    returns the modified objects (in particular [c1] and [c2]) *)  
 
+let rewrite_unif_flags = { modulo_delta = false; use_metas_eagerly = true }
+let rewrite2_unif_flags = { modulo_delta = true; use_metas_eagerly = true }
+
 let unification_rewrite c1 c2 cl but gl = 
   let (env',c1) =
     try
-      (* ~mod_delta:false to allow to mark occurences that must not be
+      (* ~flags:(false,true) to allow to mark occurences that must not be
          rewritten simply by replacing them with let-defined definitions
          in the context *)
-      w_unify_to_subterm ~mod_delta:false (pf_env gl) (c1,but) cl.evd
+      w_unify_to_subterm ~flags:rewrite_unif_flags (pf_env gl) (c1,but) cl.evd
     with
 	Pretype_errors.PretypeError _ ->
-	  (* ~mod_delta:true to make Ring work (since it really
+	  (* ~flags:(true,true) to make Ring work (since it really
              exploits conversion) *)
-	  w_unify_to_subterm ~mod_delta:true (pf_env gl) (c1,but) cl.evd
+	  w_unify_to_subterm ~flags:rewrite2_unif_flags
+	    (pf_env gl) (c1,but) cl.evd
   in
   let cl' = {cl with evd = env' } in
   let c2 = Clenv.clenv_nf_meta cl' c2 in
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli
index ecad6a574e..2dd153b3ff 100644
--- a/tactics/setoid_replace.mli
+++ b/tactics/setoid_replace.mli
@@ -79,3 +79,5 @@ val new_named_morphism :
 
 val relation_table_find : constr -> relation
 val relation_table_mem : constr -> bool
+
+val prrelation : relation -> Pp.std_ppcmds