diff options
Diffstat (limited to 'test-suite/output/goal_output.v')
| -rw-r--r-- | test-suite/output/goal_output.v | 28 |
1 files changed, 26 insertions, 2 deletions
diff --git a/test-suite/output/goal_output.v b/test-suite/output/goal_output.v index 327b80b0aa..b1ced94054 100644 --- a/test-suite/output/goal_output.v +++ b/test-suite/output/goal_output.v @@ -6,8 +6,32 @@ Print Nat.t. Timeout 1 Print Nat.t. -Lemma toto: False. 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. - |