From ba9e2688f31120adb72e3d2677d541c4b0928420 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Thu, 11 Feb 2021 19:02:59 +0100
Subject: [PATCH] adapt to coq/coq#13840

---
 tests/proofmode_ascii.v | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/tests/proofmode_ascii.v b/tests/proofmode_ascii.v
index aa2e63c33..cdefd0d4e 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.
-- 
GitLab