blob: 8d5d092333e37a667f29d80257c9daf646456b70 (
plain)
1
2
3
4
5
6
7
8
9
10
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. *)
|
