Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"

I wonder how many of us were aware of the existence of such syntax ;-)
Anyway, it is now subsumed by "rewrite by".

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

2 files changed, 92 insertions, 32 deletions

diff --git a/test-suite/parser/obj_magic.out b/test-suite/parser/obj_magic.out
index edd1e751b3..302fd6bb50 100644
--- a/test-suite/parser/obj_magic.out
+++ b/test-suite/parser/obj_magic.out
@@ -51,6 +51,9 @@ n
 vernac$absurd
 1
 n
+vernac$try
+1
+n
 vernac$none
 0
 n
@@ -76,17 +79,11 @@ vernac$int
 1
 a
 vernac$ident
-deq
-a
-vernac$ident
 H
 n
-vernac$tactic_arg_list
+vernac$simplify_eq
 1
 n
-vernac$simple_user_tac
-2
-n
 vernac$none
 0
 n
@@ -117,12 +114,24 @@ a
 vernac$ident
 b
 n
-vernac$replace_with
+vernac$hyp_location_list
+0
+n
+vernac$star
+0
+n
+vernac$clause
 2
 n
 vernac$none
 0
 n
+vernac$replace_with
+4
+n
+vernac$none
+0
+n
 vernac$solve
 3
 a
@@ -144,9 +153,15 @@ n
 vernac$binding_list
 1
 n
-vernac$none
+vernac$hyp_location_list
+0
+n
+vernac$star
 0
 n
+vernac$clause
+2
+n
 vernac$rewrite_rl
 3
 n
@@ -177,6 +192,15 @@ a
 vernac$ident
 H1
 n
+vernac$hyp_location_list
+1
+n
+vernac$none
+0
+n
+vernac$clause
+2
+n
 vernac$rewrite_rl
 3
 n
@@ -188,12 +212,6 @@ vernac$solve
 a
 vernac$int
 1
-n
-vernac$none
-0
-n
-vernac$auto
-1
 a
 vernac$ident
 H
@@ -210,11 +228,17 @@ n
 vernac$binding_list
 1
 n
-vernac$none
+vernac$hyp_location_list
 0
 n
-vernac$condrewrite_lr
-4
+vernac$star
+0
+n
+vernac$clause
+2
+n
+vernac$rewrite_lr
+3
 n
 vernac$none
 0
@@ -224,12 +248,6 @@ vernac$solve
 a
 vernac$int
 1
-n
-vernac$none
-0
-n
-vernac$auto
-1
 a
 vernac$ident
 H
@@ -249,8 +267,17 @@ a
 vernac$ident
 H2
 n
-vernac$condrewrite_lr
-4
+vernac$hyp_location_list
+1
+n
+vernac$none
+0
+n
+vernac$clause
+2
+n
+vernac$rewrite_lr
+3
 n
 vernac$none
 0
@@ -306,6 +333,36 @@ a
 vernac$int
 1
 a
+vernac$string
+_ = _
+a
+vernac$ident
+a
+a
+vernac$ident
+b
+n
+vernac$formula_list
+2
+n
+vernac$notation
+2
+a
+vernac$ident
+H
+n
+vernac$cutrewrite_lr
+2
+n
+vernac$none
+0
+n
+vernac$solve
+3
+a
+vernac$int
+1
+a
 vernac$int
 3
 a
@@ -466,16 +523,19 @@ vernac$int
 1
 a
 vernac$ident
+ring
+a
+vernac$ident
 a
 a
 vernac$ident
 b
 n
-vernac$formula_list
+vernac$tactic_arg_list
 2
 n
-vernac$ring
-1
+vernac$simple_user_tac
+2
 n
 vernac$none
 0
@@ -544,6 +604,6 @@ vernac$hintrewrite
 4
 n
 vernac$command_list
-20
+21
 e
 blabla
diff --git a/test-suite/parser/obj_magic.v b/test-suite/parser/obj_magic.v
index 7d60bbd977..7f0c23af66 100644
--- a/test-suite/parser/obj_magic.v
+++ b/test-suite/parser/obj_magic.v
@@ -6,8 +6,8 @@ injection H.
 replace a with b.
 rewrite <- H with (a := b).
 rewrite <- H with (a := b) in H1.
-conditional (auto) rewrite H with (1 := b).
-conditional (auto) rewrite H with (1 := b) in H2.
+rewrite H with (1 := b).
+rewrite H with (1 := b) in H2.
 dependent rewrite H.
 cutrewrite (a = b).
 cutrewrite (a = b) in H.