Merge PR #9200: [ssr] make `>` stand alone

2 files changed, 38 insertions, 0 deletions

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.