diff --git a/tests/proofmode_ascii.v b/tests/proofmode_ascii.v
index cdefd0d4ea407a53df6429a0f4046e38e752c986..e29a22860f68e44a162e35c12d4a5cb4cc78ab32 100644
--- a/tests/proofmode_ascii.v
+++ b/tests/proofmode_ascii.v
@@ -297,7 +297,9 @@ Lemma test_entails_annot_sections_space_close P :
   (P -|-@{PROP} P ) /\ (-|-@{PROP} ) P P.
 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".
 Lemma p1 : forall P, True -> P |- P.
 Proof.
@@ -352,6 +354,4 @@ Proof.
   Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
 Abort.
 
-Set Printing Notations. Unset Printing Raw Literals.
-
 End parsing_tests.