Ajout fonction clenv_conv_leq pour résoudre les pbs de la forme

"R ?1 ... ?n <= T". Utilisation de cette fonction dans Setoid_replace au
au lieu de w_unify (suggestion de GG).


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

3 files changed, 18 insertions, 20 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index d79910c99e..b18034b50c 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -127,6 +127,16 @@ let clenv_environments_evars env evd bound c =
   in 
   clrec (evd,[]) bound c
 
+let clenv_conv_leq env sigma t c bound =
+  let ty = Retyping.get_type_of env sigma c in
+  let evd = Evd.create_evar_defs sigma in
+  let evars,args,_ = clenv_environments_evars env evd (Some bound) ty in
+  let evars = Evarconv.the_conv_x_leq env t (applist (c,args)) evars in
+  let evars,_ = Evarconv.consider_remaining_unif_problems env evars in
+  let args = List.map (whd_evar (Evd.evars_of evars)) args in
+  check_evars env sigma evars (applist (c,args));
+  args
+
 let mk_clenv_from_n gls n (c,cty) =
   let evd = create_evar_defs gls.sigma in
   let (env,args,concl) = clenv_environments evd n cty in
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index 98950458ea..b855ee7e0a 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -125,6 +125,10 @@ val clenv_environments :
 val clenv_environments_evars :
  env -> evar_defs -> int option -> types -> evar_defs * constr list * types
 
+(* [clenv_conv_leq env sigma t c n] looks for c1...cn s.t. [t <= c c1...cn] *)
+val clenv_conv_leq :
+ env -> evar_map -> types -> constr -> int -> constr list
+
 (* if the clause is a product, add an extra meta for this product *)
 exception NotExtensibleClause
 val clenv_push_prod : clausenv -> clausenv
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 5da0bb047a..99cf25779a 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -727,26 +727,10 @@ let unify_relation_carrier_with_type env rel t =
      if rel.rel_quantifiers_no = 0 && is_conv env Evd.empty rel.rel_a t then
       [||] 
      else
-      begin
-        let evars,args,instantiated_rel_a =
-         let ty = Typing.type_of env Evd.empty rel.rel_a in
-         let evd = Evd.create_evar_defs Evd.empty in
-         let evars,args,concl =
-          Clenv.clenv_environments_evars env evd
-           (Some rel.rel_quantifiers_no) ty
-         in
-          evars, args,
-          nf_betaiota
-           (match args with [] -> rel.rel_a | _ -> applist (rel.rel_a,args))
-        in
-         let evars' =
-          w_unify true (*??? or false? *) env Reduction.CONV (*??? or cumul? *)
-           ~mod_delta:true (*??? or true? *) t instantiated_rel_a evars in
-         let args' =
-          List.map (Reductionops.nf_evar (Evd.evars_of evars')) args
-         in
-          Array.of_list args'
-      end
+       let args =
+         Clenv.clenv_conv_leq env Evd.empty t rel.rel_a rel.rel_quantifiers_no
+       in
+       Array.of_list args
  in
   apply_to_relation args rel