1 files changed, 16 insertions, 0 deletions
diff --git a/test-suite/success/remember.v b/test-suite/success/remember.v
new file mode 100644
index 00000000..0befe054
--- /dev/null
+++ b/test-suite/success/remember.v
@@ -0,0 +1,16 @@
+(* Testing remember and co *)
+
+Lemma A : forall (P: forall X, X -> Prop), P nat 0 -> P nat 0.
+intros.
+Fail remember nat as X.
+Fail remember nat as X in H. (* This line used to succeed in 8.3 *)
+Fail remember nat as X.
+Abort.
+
+(* Testing Ltac interpretation of remember (was not working up to r16181) *)
+
+Goal (1 + 2 + 3 = 6).
+let name := fresh "fresh" in
+remember (1 + 2) as x eqn:name.
+rewrite fresh.
+Abort.