From e5fe4569f3eaeaa4e1ce377989e19f1f2c176da9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 28 Apr 2016 00:02:32 +0200
Subject: An example for cd139311e, showing a consequence of not converting
 constants up to their canonical name (taken from Daniel's formalization of
 Puiseux theorem).

---
 test-suite/success/remember.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/test-suite/success/remember.v b/test-suite/success/remember.v
index 0befe054a3..b26a9ff1eb 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.           
+                
-- 
cgit v1.2.3