diff --git a/tests/proofmode_ascii.v b/tests/proofmode_ascii.v
index aa2e63c33a6526f5bbfc487c08cc26beb2397a7d..cdefd0d4ea407a53df6429a0f4046e38e752c986 100644
--- a/tests/proofmode_ascii.v
+++ b/tests/proofmode_ascii.v
@@ -301,57 +301,57 @@ Proof. naive_solver. Qed.
 Check "p1".
 Lemma p1 : forall P, True -> P |- P.
 Proof.
-  Unset Printing Notations. Show. Set Printing Notations.
+  Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
 Abort.
 
 Check "p2".
 Lemma p2 : forall P, True /\ (P |- P).
 Proof.
-  Unset Printing Notations. Show. Set Printing Notations.
+  Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
 Abort.
 
 Check "p3".
 Lemma p3 : exists P, P |- P.
 Proof.
-  Unset Printing Notations. Show. Set Printing Notations.
+  Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
 Abort.
 
 Check "p4".
 Lemma p4 : |-@{PROP} exists (x : nat), ⌜x = 0⌝.
 Proof.
-  Unset Printing Notations. Show. Set Printing Notations.
+  Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
 Abort.
 
 Check "p5".
 Lemma p5 : |-@{PROP} exists (x : nat), ⌜forall y : nat, y = y⌝.
 Proof.
-  Unset Printing Notations. Show. Set Printing Notations.
+  Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
 Abort.
 
 Check "p6".
 Lemma p6 : exists! (z : nat), |-@{PROP} exists (x : nat), ⌜forall y : nat, y = y⌝ ** ⌜z = 0⌝.
 Proof.
-  Unset Printing Notations. Show. Set Printing Notations.
+  Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
 Abort.
 
 Check "p7".
 Lemma p7 : forall (a : nat), a = 0 -> forall y, True |-@{PROP} ⌜y >= 0⌝.
 Proof.
-  Unset Printing Notations. Show. Set Printing Notations.
+  Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
 Abort.
 
 Check "p8".
 Lemma p8 : forall (a : nat), a = 0 -> forall y, |-@{PROP} ⌜y >= 0⌝.
 Proof.
-  Unset Printing Notations. Show. Set Printing Notations.
+  Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
 Abort.
 
 Check "p9".
 Lemma p9 : forall (a : nat), a = 0 -> forall y : nat, |-@{PROP} forall z : nat, ⌜z >= 0⌝.
 Proof.
-  Unset Printing Notations. Show. Set Printing Notations.
+  Unset Printing Notations. Set Printing Raw Literals. Show. Set Printing Notations. Unset Printing Raw Literals.
 Abort.
 
-Set Printing Notations.
+Set Printing Notations. Unset Printing Raw Literals.
 
 End parsing_tests.