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
---
 proofs/tacexpr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index a63fd1aebb..f74413704b 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -194,7 +194,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
 
   (* Equality and inversion *)
   | TacRewrite of 
-      evars_flag * (bool * multi * 'constr with_bindings) list * 'id gclause
+      evars_flag * (bool * multi * 'constr with_bindings) list * 'id gclause * 'tac option
   | TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis
       
   (* For ML extensions *)
-- 
cgit v1.2.3