diff options
| author | Guillaume Melquiond | 2021-02-23 17:51:07 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2021-02-24 00:08:09 +0100 |
| commit | b31c4fa57eac8162ad6b6e03f75b13afd9b76db7 (patch) | |
| tree | e379b0769b89831d4756733cc068b2a2ff3da206 /test-suite | |
| parent | f89f0eb4717b64f10bdd0a0edc9e93b949bcb33d (diff) | |
Use Reductionops.clos_whd_flags in vm_compute and native_compute.
Diffstat (limited to 'test-suite')
| -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. |