diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_13841.v | 11 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_7631.v | 6 |
2 files changed, 17 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_13841.v b/test-suite/bugs/closed/bug_13841.v new file mode 100644 index 0000000000..60fca8b49c --- /dev/null +++ b/test-suite/bugs/closed/bug_13841.v @@ -0,0 +1,11 @@ +Goal True. +evar (p : bool). +unify ?p true. +let v := eval vm_compute in (orb p false) in +match v with true => idtac end. +assert (orb p false = true). +vm_compute. +match goal with |- true = _ => idtac end. +easy. +easy. +Qed. 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. |