[ssr] under: Add a fancy test with several kinds of side-conditions

1 files changed, 19 insertions, 0 deletions

diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v
index cc85b96a3a..190277aa31 100644
--- a/test-suite/ssr/under.v
+++ b/test-suite/ssr/under.v
@@ -149,3 +149,22 @@ under i: eq_bigr by move/eqP=>{1}->. (* the 2nd occ should not be touched *)
 simpl.
 myadmit.
 Qed.
+
+Lemma test_foo (f1 f2 : nat -> nat) (f_eq : forall n, f1 n = f2 n)
+      (G : (nat -> nat) -> nat)
+      (Lem : forall f1 f2 : nat -> nat,
+          True ->
+          (forall n, f1 n = f2 n) ->
+          False = False ->
+          G f1 = G f2) :
+  G f1 = G f2.
+Proof.
+(*
+under x: Lem.
+- done.
+- rewrite f_eq; over.
+- done.
+ *)
+under x: Lem by [done|rewrite f_eq|done].
+done.
+Qed.