1 files changed, 13 insertions, 0 deletions
diff --git a/test-suite/success/remember.v b/test-suite/success/remember.v
index 0befe054a..b26a9ff1e 100644
--- a/test-suite/success/remember.v
+++ b/test-suite/success/remember.v
@@ -14,3 +14,16 @@ let name := fresh "fresh" in
 remember (1 + 2) as x eqn:name.
 rewrite fresh.
 Abort.
+
+(* An example which was working in 8.4 but failing in 8.5 and 8.5pl1 *)
+                  
+Module A.
+Axiom N : nat.
+End A.
+Module B.
+Include A.
+End B.
+Goal id A.N = B.N.
+reflexivity.
+Qed.           
+