summaryrefslogtreecommitdiff
path: root/test-suite/interactive
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/interactive')
-rw-r--r--test-suite/interactive/4289.v14
-rw-r--r--[-rwxr-xr-x]test-suite/interactive/ParalITP_smallproofs.v0
2 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/interactive/4289.v b/test-suite/interactive/4289.v
new file mode 100644
index 00000000..610a509c
--- /dev/null
+++ b/test-suite/interactive/4289.v
@@ -0,0 +1,14 @@
+(* Checking backtracking with modules which used to fail due to an
+ hash-consing bug *)
+
+Module Type A.
+ Axiom B : nat.
+End A.
+Module C (a : A).
+ Include a.
+ Definition c : nat := B.
+End C.
+Back 4.
+Module C (a : A).
+ Include a.
+ Definition c : nat := B.
diff --git a/test-suite/interactive/ParalITP_smallproofs.v b/test-suite/interactive/ParalITP_smallproofs.v
index 0d75d52a..0d75d52a 100755..100644
--- a/test-suite/interactive/ParalITP_smallproofs.v
+++ b/test-suite/interactive/ParalITP_smallproofs.v