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

2 files changed, 14 insertions, 0 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index d79910c99..b18034b50 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 98950458e..b855ee7e0 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