From 70894b275f1dbaf73d54770bb4311a146c9514d8 Mon Sep 17 00:00:00 2001
From: barras
Date: Tue, 5 Mar 2002 10:59:15 +0000
Subject: assert failure avec Conditional Rewrite

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2513 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/equality.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/tactics/equality.ml b/tactics/equality.ml
index ee01a3b1fd..de98abd610 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -106,8 +106,8 @@ let dyn_conditional_rewrite lft2rgt = function
       tactic_com_bind_list 
 	(conditional_rewrite lft2rgt (Tacinterp.interp tac)) 
 	(com,binds)
-  | [(Tacexp tac); (Constr c);(Cbindings binds)] -> 
-      conditional_rewrite lft2rgt (Tacinterp.interp tac) (c,binds)
+  | [(Tac (tac,_)); (Constr c);(Cbindings binds)] -> 
+      conditional_rewrite lft2rgt tac (c,binds)
   | _ -> assert false
                  
 let v_rewriteLR = hide_tactic "RewriteLR" dyn_rewriteLR
@@ -162,8 +162,8 @@ let dyn_conditional_rewrite_in lft2rgt = function
       tactic_com_bind_list 
 	(conditional_rewrite_in lft2rgt id (Tacinterp.interp tac)) 
 	(com,binds)
-  | [(Tacexp tac); Identifier id; (Constr c);(Cbindings binds)] -> 
-      conditional_rewrite_in lft2rgt id (Tacinterp.interp tac) (c,binds)
+  | [(Tac (tac,_)); Identifier id; (Constr c);(Cbindings binds)] -> 
+      conditional_rewrite_in lft2rgt id tac (c,binds)
   | _ -> assert false
 
 let rewriteLR_in_tac =  hide_tactic "RewriteLRin" (dyn_rewrite_in true)
-- 
cgit v1.2.3