Fix wrong environment bug in test for setoid_rewrite or rewrite.

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

1 files changed, 3 insertions, 2 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index ba982ccee..5212711ae 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -116,12 +116,13 @@ let general_rewrite_ebindings_clause cls lft2rgt occs (c,l) with_evars gl =
     let ctype = pf_apply get_type_of gl c in 
     let env = pf_env gl in
     let sigma = project gl in 
-    let t = snd (decompose_prod (whd_betaiotazeta ctype)) in
+    let rels, t = decompose_prod (whd_betaiotazeta ctype) in
       match match_with_equation t with
       | Some (hdcncl,_) -> (* Fast path: direct leibniz rewrite *)
 	  leibniz_rewrite_ebindings_clause cls lft2rgt (c,l) with_evars gl hdcncl
       | None ->
-	  let _,t' = splay_prod env sigma t in (* Search for underlying eq *)
+	  let env' = List.fold_left (fun env (n,t) -> push_rel (n, None, t) env) env rels in
+	  let _,t' = splay_prod env' sigma t in (* Search for underlying eq *)
 	    match match_with_equation t' with
 	    | Some (hdcncl,_) -> (* Maybe a setoid relation with eq inside *)
 		if l = NoBindings && !is_applied_setoid_relation t then