aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/auto.v
blob: a77b7b82e62097211d2f6eecc5e6d8f83bf16d7e (plain)
1
2
3
4
5
6
7
8
9
10
11
(* testing info/debug auto/eauto *)

Goal False \/ (True -> True).
info_auto.
Undo.
debug auto.
Undo.
info_eauto.
Undo.
debug eauto.
Qed.