From 3074967fd01acc5987eb2ea648fcfe32aeca1749 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 12 Jul 2016 12:27:53 +0200
Subject: Few tests for e-variants of assert, set, remember.

---
 test-suite/success/forward.v | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 test-suite/success/forward.v

diff --git a/test-suite/success/forward.v b/test-suite/success/forward.v
new file mode 100644
index 0000000000..0ed5b524f3
--- /dev/null
+++ b/test-suite/success/forward.v
@@ -0,0 +1,18 @@
+(* Testing forward reasoning *)
+
+Goal 0=0.
+Fail assert (_ = _).
+eassert (_ = _)by reflexivity.
+eassumption.
+Qed.
+
+Goal 0=0.
+Fail set (S ?[nl]).
+eset (S ?[n]).
+remember (S ?n) as x.
+instantiate (n:=0).
+Fail remember (S (S _)).
+eremember (S (S ?[x])).
+instantiate (x:=0).
+reflexivity.
+Qed.
-- 
cgit v1.2.3