1 files changed, 25 insertions, 0 deletions
diff --git a/mathcomp/ssrtest/ssrsyntax1.v b/mathcomp/ssrtest/ssrsyntax1.v
new file mode 100644
index 0000000..64e78da
--- /dev/null
+++ b/mathcomp/ssrtest/ssrsyntax1.v
@@ -0,0 +1,25 @@
+(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
+Require ssreflect.
+Require Import Arith.
+
+Goal (forall a b, a + b = b + a).
+intros.
+rewrite plus_comm, plus_comm.
+split.
+Abort.
+
+Module Foo.
+Import ssreflect.
+
+Goal (forall a b, a + b = b + a).
+intros.
+rewrite 2![_ + _]plus_comm. 
+split.
+Abort.
+End Foo.
+
+Goal (forall a b, a + b = b + a).
+intros.
+rewrite plus_comm, plus_comm.
+split.
+Abort.
+\ No newline at end of file