blob: 92917cdfc7fede3f4301f874eb5829933c628be4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
(* testing info/debug auto/eauto *)
Goal False \/ (True -> True).
info_auto.
Undo.
debug auto.
Undo.
info_eauto.
Undo.
debug eauto.
Qed.
Goal True.
info_trivial.
Qed.
|