aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-05-30 18:20:52 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-04 22:45:22 +0200
commit7ada864b7728c9c94b7ca9856b6b2c89feb0214e (patch)
tree0bcb36c170ae6f3c960bdc9a7bab9e3fefcc42bb /test-suite
parentf6538f1a7f8ad2bdc0bc446d4ca35078d55d63ee (diff)
Fix #7631: native_compute fails to compile an example in Coq 8.8
Dependency analysis for separate compilation was not iterated properly on rel_context and named_context.
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/7631.v21
1 files changed, 21 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/7631.v b/test-suite/bugs/closed/7631.v
new file mode 100644
index 000000000..34eb8b867
--- /dev/null
+++ b/test-suite/bugs/closed/7631.v
@@ -0,0 +1,21 @@
+Module NamedContext.
+
+Definition foo := true.
+
+Section Foo.
+
+Let bar := foo.
+
+Eval native_compute in bar.
+
+End Foo.
+
+End NamedContext.
+
+Module RelContext.
+
+Definition foo := true.
+
+Definition bar (x := foo) := Eval native_compute in x.
+
+End RelContext.