Fix bug #2317: setoid_rewrite ignored binding lists. Slightly

generalize the interface of Clenv to be able to use the existing
treatment of bindings. Clenv functions did not use goals conclusions
but insisted on getting goals anyway (which is even more problematic as
goals appear in evar maps now).


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

1 files changed, 11 insertions, 7 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 48d78d858..dade69865 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -462,18 +462,22 @@ let clenv_constrain_dep_args hyps_only bl clenv =
 (****************************************************************)
 (* Clausal environment for an application *)
 
-let make_clenv_binding_gen hyps_only n gls (c,t) = function
+let make_clenv_binding_gen hyps_only n env sigma (c,t) = function
   | ImplicitBindings largs ->
-      let clause = mk_clenv_from_n gls n (c,t) in
+      let clause = mk_clenv_from_env env sigma n (c,t) in
       clenv_constrain_dep_args hyps_only largs clause
   | ExplicitBindings lbind ->
-      let clause = mk_clenv_rename_from_n gls n (c,t) in
-      clenv_match_args lbind clause
+      let clause = mk_clenv_from_env env sigma n 
+	(c,rename_bound_vars_as_displayed [] t) 
+      in clenv_match_args lbind clause
   | NoBindings ->
-      mk_clenv_from_n gls n (c,t)
+      mk_clenv_from_env env sigma n (c,t)
 
-let make_clenv_binding_apply gls n = make_clenv_binding_gen true n gls
-let make_clenv_binding = make_clenv_binding_gen false None
+let make_clenv_binding_env_apply env sigma n =
+  make_clenv_binding_gen true n env sigma
+	
+let make_clenv_binding_apply gls n = make_clenv_binding_gen true n (pf_env gls) gls.sigma
+let make_clenv_binding gls = make_clenv_binding_gen false None (pf_env gls) gls.sigma
 
 (****************************************************************)
 (* Pretty-print *)