From 6835590f6e0a8e96719c7f37ef6f8bb789bd349b Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Wed, 3 Apr 2019 01:07:11 +0200
Subject: [ssr] Add small output test for "under eq_G => m do rewrite subnn"

---
 test-suite/output/ssr_under.out |  2 ++
 test-suite/output/ssr_under.v   | 15 +++++++++++++++
 2 files changed, 17 insertions(+)
 create mode 100644 test-suite/output/ssr_under.out
 create mode 100644 test-suite/output/ssr_under.v

diff --git a/test-suite/output/ssr_under.out b/test-suite/output/ssr_under.out
new file mode 100644
index 0000000000..8532b62a54
--- /dev/null
+++ b/test-suite/output/ssr_under.out
@@ -0,0 +1,2 @@
+'Under[ m - m ]
+(G (fun _ : nat => 0) n >= 0)
diff --git a/test-suite/output/ssr_under.v b/test-suite/output/ssr_under.v
new file mode 100644
index 0000000000..b11dd1509c
--- /dev/null
+++ b/test-suite/output/ssr_under.v
@@ -0,0 +1,15 @@
+From Coq Require Import ssreflect.
+
+Axiom subnn : forall n : nat, n - n = 0.
+Parameter G : (nat -> nat) -> nat -> nat.
+Axiom eq_G :
+  forall F1 F2 : nat -> nat,
+    (forall n : nat, F1 n = F2 n) ->
+    forall n : nat, G F1 n = G F2 n.
+
+Ltac show := match goal with [|-?g] => idtac g end.
+
+Lemma example_G (n : nat) : G (fun n => n - n) n >= 0.
+under eq_G => m do show; rewrite subnn.
+show.
+Abort.
-- 
cgit v1.2.3