diff options
Diffstat (limited to 'test-suite/bugs/closed/bug_7631.v')
| -rw-r--r-- | test-suite/bugs/closed/bug_7631.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_7631.v b/test-suite/bugs/closed/bug_7631.v index 93aeb83e28..14ab4de9b7 100644 --- a/test-suite/bugs/closed/bug_7631.v +++ b/test-suite/bugs/closed/bug_7631.v @@ -21,3 +21,9 @@ Definition bar (x := foo) := Eval native_compute in x. Definition barvm (x := foo) := Eval vm_compute in x. End RelContext. + +Definition bar (t:=_) (x := true : t) := Eval native_compute in x. +Definition barvm (t:=_) (x := true : t) := Eval vm_compute in x. + +Definition baz (z:nat) (t:=_ z) (x := true : t) := Eval native_compute in x. +Definition bazvm (z:nat) (t:=_ z) (x := true : t) := Eval vm_compute in x. |