In "simpl c" and "change c with d", c can be a pattern.

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

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 000000000..73888da9a
--- /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 000000000..5f1926f14
--- /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 cea017122..c72ee875a 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.