diff options
| author | coqbot-app[bot] | 2021-03-11 11:57:46 +0000 |
|---|---|---|
| committer | GitHub | 2021-03-11 11:57:46 +0000 |
| commit | d33266649d285b7d8ba5a7093319faa6132d6bc9 (patch) | |
| tree | a49c779eeddeb56909d3dd85f8423fde133a88fb /test-suite | |
| parent | a40631f9fbcd0ef8c1a716010be48e3f650e8955 (diff) | |
| parent | b31c4fa57eac8162ad6b6e03f75b13afd9b76db7 (diff) | |
Merge PR #13854: Normalize evars during bytecode compilation.
Reviewed-by: SkySkimmer
Ack-by: ppedrot
Ack-by: ejgallego
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. |