test-suite/output/auto.v


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.