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

1 files changed, 4 insertions, 20 deletions

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