Skip to content
Snippets Groups Projects
Commit bc2e668d authored by Ralf Jung's avatar Ralf Jung
Browse files

explain why we reconfigure printing all the time

parent 935e3488
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 3 additions and 3 deletions
tests/proofmode_ascii.v
+ 3
− 3
View file @ bc2e668d
...@@ -297,7 +297,9 @@ Lemma test_entails_annot_sections_space_close P : ...@@ -297,7 +297,9 @@ Lemma test_entails_annot_sections_space_close P :
(P -|-@{PROP} P ) /\ (-|-@{PROP} ) P P. (P -|-@{PROP} P ) /\ (-|-@{PROP} ) P P.
Proof. naive_solver. Qed. Proof. naive_solver. Qed.
(* Make sure these all parse as they should.
To make the [Check] print correctly, we need to set and reset the printing
settings each time. *)
Check "p1". Check "p1".
Lemma p1 : forall P, True -> P |- P. Lemma p1 : forall P, True -> P |- P.
Proof. Proof.
...@@ -352,6 +354,4 @@ Proof. ...@@ -352,6 +354,4 @@ Proof.
Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals. Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
Abort. Abort.
Set Printing Notations. Unset Printing Raw Literals.
End parsing_tests. End parsing_tests.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment