blob: b1ced94054c66d5c8bd20842a35a5776c31b6bb5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
(* From
- https://coq.inria.fr/bugs/show_bug.cgi?id=5529
- https://coq.inria.fr/bugs/show_bug.cgi?id=5537
*)
Print Nat.t.
Timeout 1 Print Nat.t.
Set Printing All.
Lemma toto: True/\True.
Proof.
split.
Show.
Set Printing Goal Names.
Show.
Unset Printing Goal Names.
assert True.
- idtac.
Show.
Set Printing Goal Names.
Show.
Set Printing Unfocused.
Show.
Unset Printing Goal Names.
Show.
Unset Printing Unfocused.
auto.
Show.
Set Printing Goal Names.
Show.
Unset Printing Goal Names.
- auto.
Show.
Set Printing Goal Names.
Show.
Unset Printing Goal Names.
Abort.
|
