diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-01-22 09:45:12 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-01-22 09:45:12 +0100 |
| commit | 35a275e22b72abba344b837e7276af8057d5da2c (patch) | |
| tree | d04e278cfc4a018be1a22b902aeeb8992027c760 /test-suite/bugs | |
| parent | e0805eac59ee4c6c2eafae1d6b7f91530104f18f (diff) | |
| parent | d8652efca406c852ebc27cb27c903d9a6a4b2532 (diff) | |
Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction.
Diffstat (limited to 'test-suite/bugs')
| -rw-r--r-- | test-suite/bugs/opened/6393.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/6393.v b/test-suite/bugs/opened/6393.v new file mode 100644 index 000000000..8d5d09233 --- /dev/null +++ b/test-suite/bugs/opened/6393.v @@ -0,0 +1,11 @@ +(* These always worked. *) +Goal prod True True. firstorder. Qed. +Goal True -> @sigT True (fun _ => True). firstorder. Qed. +Goal prod True True. dtauto. Qed. +Goal prod True True. tauto. Qed. + +(* These should work. *) +Goal @sigT True (fun _ => True). dtauto. Qed. +(* These should work, but don't *) +(* Goal @sigT True (fun _ => True). firstorder. Qed. *) +(* Goal @sigT True (fun _ => True). tauto. Qed. *) |