1 files changed, 30 insertions, 0 deletions
diff --git a/test-suite/success/rewrite_iterated.v b/test-suite/success/rewrite_iterated.v
new file mode 100644
index 00000000..962dada3
--- /dev/null
+++ b/test-suite/success/rewrite_iterated.v
@@ -0,0 +1,30 @@
+Require Import Arith Omega.
+
+Lemma test : forall p:nat, p<>0 -> p-1+1=p.
+Proof.
+ intros; omega.
+Qed.
+
+(** Test of new syntax for rewrite : ! ? and so on... *)
+
+Lemma but : forall a b c, a<>0 -> b<>0 -> c<>0 ->
+ (a-1+1)+(b-1+1)+(c-1+1)=a+b+c.
+Proof.
+intros.
+rewrite test.
+Undo.
+rewrite test,test.
+Undo.
+rewrite 2 test. (* or rewrite 2test or rewrite 2!test *)
+Undo.
+rewrite 2!test,2?test.
+Undo.
+(*rewrite 4!test.  --> error *)
+rewrite 3!test.
+Undo.
+rewrite <- 3?test.
+Undo.
+(*rewrite <-?test. --> loops*)
+rewrite !test by auto.
+reflexivity.
+Qed.