From 43fede22d500a7234a82aaae77adfebff8006c4f Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 9 Jun 2010 18:23:23 +0000
Subject: 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
---
 proofs/clenv.ml  | 18 +++++++++++-------
 proofs/clenv.mli |  4 ++++
 2 files changed, 15 insertions(+), 7 deletions(-)

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 48d78d8589..dade69865c 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 *)
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index afda6d9315..209024c9c4 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -97,6 +97,10 @@ val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv
 (** the arity of the lemma is fixed 
    the optional int tells how many prods of the lemma have to be used 
    use all of them if None *)
+val make_clenv_binding_env_apply :
+  env -> evar_map -> int option -> constr * constr -> constr bindings ->
+   clausenv
+
 val make_clenv_binding_apply :
   Goal.goal sigma -> int option -> constr * constr -> constr bindings ->
    clausenv
-- 
cgit v1.2.3