From d8b8893f7700e17700ca40c52b69a0a554b2da2f Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Mon, 25 Feb 2019 02:25:31 +0100
Subject: [ssr] under: Add a fancy test with several kinds of side-conditions

---
 test-suite/ssr/under.v | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

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.
-- 
cgit v1.2.3