2 files changed, 28 insertions, 0 deletions
diff --git a/test-suite/output/simpl.out b/test-suite/output/simpl.out
new file mode 100644
index 0000000000..73888da9a0
--- /dev/null
+++ b/test-suite/output/simpl.out
@@ -0,0 +1,15 @@
+1 subgoal
+  
+  x : nat
+  ============================
+   x = S x
+1 subgoal
+  
+  x : nat
+  ============================
+   0 + x = S x
+1 subgoal
+  
+  x : nat
+  ============================
+   x = 1 + x
diff --git a/test-suite/output/simpl.v b/test-suite/output/simpl.v
new file mode 100644
index 0000000000..5f1926f142
--- /dev/null
+++ b/test-suite/output/simpl.v
@@ -0,0 +1,13 @@
+(* Simpl with patterns *)
+
+Goal forall x, 0+x = 1+x.
+intro x.
+simpl (_ + x).
+Show.
+Undo.
+simpl (_ + x) at 2.
+Show.
+Undo.
+simpl (0 + _).
+Show.
+Undo.