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
---
 parsing/g_tactic.ml4 | 12 ++++++++----
 parsing/pptactic.ml  |  5 +++--
 2 files changed, 11 insertions(+), 6 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index a4e5d4cb83..96db00e3e4 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -319,6 +319,10 @@ GEXTEND Gram
     [ [ IDENT "by"; tac = tactic_expr LEVEL "3" -> TacComplete tac
       | -> TacId [] ] ]
   ;
+  opt_by_tactic:
+    [ [ IDENT "by"; tac = tactic_expr LEVEL "3" -> Some tac
+    | -> None ] ]
+  ;
   rename : 
     [ [ id1 = id_or_meta; IDENT "into"; id2 = id_or_meta -> (id1,id2) ] ]
   ;
@@ -471,10 +475,10 @@ GEXTEND Gram
       | IDENT "transitivity"; c = constr -> TacTransitivity c
 
       (* Equality and inversion *)
-      | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause ->
-	  TacRewrite (false,l,cl)
-      | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause ->
-	  TacRewrite (true,l,cl)
+      | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause; t=opt_by_tactic ->
+	  TacRewrite (false,l,cl,t)
+      | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause; t=opt_by_tactic ->
+	  TacRewrite (true,l,cl,t)
       | IDENT "dependent"; k =
 	  [ IDENT "simple"; IDENT "inversion" -> SimpleInversion
 	  | IDENT "inversion" -> FullInversion
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index da915a5cc3..448b78e262 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -821,14 +821,15 @@ and pr_atom1 = function
   | TacTransitivity c -> str "transitivity" ++ pr_constrarg c
 
   (* Equality and inversion *)
-  | TacRewrite (ev,l,cl) -> 
+  | TacRewrite (ev,l,cl,by) -> 
       hov 1 (str (if ev then "erewrite" else "rewrite") ++ 
 	     prlist_with_sep
 	     (fun () -> str ","++spc())
 	     (fun (b,m,c) -> 
 		pr_orient b ++ spc() ++ pr_multi m ++ pr_with_bindings c)
 	     l
-	     ++ pr_clauses pr_ident cl) 
+	     ++ pr_clauses pr_ident cl
+	     ++	(match by with Some by -> pr_by_tactic (pr_tac_level ltop) by | None -> mt())) 
   | TacInversion (DepInversion (k,c,ids),hyp) ->
       hov 1 (str "dependent " ++ pr_induction_kind k ++ spc () ++
       pr_quantified_hypothesis hyp ++
-- 
cgit v1.2.3