From 235253d0a119cb97daa636646336d307bc96d5b7 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 11 Dec 2018 17:21:46 +0100
Subject: [ssr] make > a stand alone intro pattern

---
 test-suite/ssr/ipat_fast_any.v | 21 +++++++++++++++++++++
 test-suite/ssr/ipat_fastid.v   | 17 +++++++++++++++++
 2 files changed, 38 insertions(+)
 create mode 100644 test-suite/ssr/ipat_fast_any.v

(limited to 'test-suite')

diff --git a/test-suite/ssr/ipat_fast_any.v b/test-suite/ssr/ipat_fast_any.v
new file mode 100644
index 0000000000..a50984c7c0
--- /dev/null
+++ b/test-suite/ssr/ipat_fast_any.v
@@ -0,0 +1,21 @@
+Require Import ssreflect.
+
+Goal forall y x : nat, x = y -> x = x.
+Proof.
+move=> + > ->. match goal with |- forall y, y = y => by [] end.
+Qed.
+
+Goal forall y x : nat, le x y -> x = y.
+Proof.
+move=> > [|].
+  by [].
+match goal with |- forall a, _ <= a -> _ = S a => admit end.
+Admitted.
+
+Goal forall y x : nat, le x y -> x = y.
+Proof.
+move=> y x.
+case E: x => >.
+  admit.
+match goal with |- S _ <= y -> S _ = y => admit end.
+Admitted.
diff --git a/test-suite/ssr/ipat_fastid.v b/test-suite/ssr/ipat_fastid.v
index 8dc0c6cf0b..b0985a0d2f 100644
--- a/test-suite/ssr/ipat_fastid.v
+++ b/test-suite/ssr/ipat_fastid.v
@@ -11,6 +11,15 @@ lazymatch goal with
 end.
 Qed.
 
+Lemma simple2 :
+  forall x, 3 <= x -> forall y, odd (y+x) -> x = y -> True.
+Proof.
+move=> >; move=>x_ge_3; move=> >; move=>xy_odd.
+lazymatch goal with
+| |- ?x = ?y -> True => done
+end.
+Qed.
+
 
 Definition stuff x := 3 <= x -> forall y, odd (y+x) -> x = y -> True.
 
@@ -22,6 +31,14 @@ lazymatch goal with
 end.
 Qed.
 
+Lemma harder2 : forall x, stuff x.
+Proof.
+move=> >; move=>x_ge_3;move=> >; move=>xy_odd.
+lazymatch goal with
+| |- ?x = ?y -> True => done
+end.
+Qed.
+
 Lemma homotop : forall x : nat, forall e : x = x, e = e -> True.
 Proof.
 move=> >eq_ee.
-- 
cgit v1.2.3