From ec850ff623801e514b3ed0a42beb6f7984992520 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 7 Mar 2008 16:32:12 +0000
Subject: Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As
 part of the fix I added an optional "by" annotation for rewrite to solve said
 conditions in the same tactic call. Most of the theories have been updated,
 only FSets is missing, Pierre will take care of it.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10634 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/equality.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'tactics/equality.mli')

diff --git a/tactics/equality.mli b/tactics/equality.mli
index 846487f964..91a0d33c6d 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -53,7 +53,8 @@ val general_rewrite_in          :
 val general_multi_rewrite : 
   bool -> evars_flag -> constr with_ebindings -> clause -> tactic
 val general_multi_multi_rewrite : 
-  evars_flag -> (bool * multi * constr with_ebindings) list -> clause -> tactic
+  evars_flag -> (bool * multi * constr with_ebindings) list -> clause -> 
+  tactic option -> tactic
 
 val conditional_rewrite : bool -> tactic -> constr with_ebindings -> tactic
 val conditional_rewrite_in :
-- 
cgit v1.2.3