3 files changed, 34 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.
diff --git a/test-suite/success/change.v b/test-suite/success/change.v
index cea017122e..c72ee875af 100644
--- a/test-suite/success/change.v
+++ b/test-suite/success/change.v
@@ -4,3 +4,9 @@ Goal let a := 0+0 in a=a.
 intro.
 change 0 in (value of a).
 change ((fun A:Type => A) nat) in (type of a).
+Abort.
+
+Goal forall x, 2 + S x = 1 + S x.
+intro. 
+change (?u + S x) with (S (u + x)). 
+Abort.