diff options
Diffstat (limited to 'test-suite/bugs/closed/7631.v')
-rw-r--r-- | test-suite/bugs/closed/7631.v | 21 |
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. |