diff options
Diffstat (limited to 'test-suite/bugs/opened/6393.v')
| -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 00000000..8d5d0923 --- /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. *) |