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 00000000..34eb8b86
--- /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.