Merge PR #7643: Fix #7631: native_compute fails to compile an example in Coq 8.8

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 0000000000..34eb8b8676
--- /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.