From bc2e668d72dbbca5ecae2e95229004e7e38bcaa0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 12 Feb 2021 10:02:06 +0100
Subject: [PATCH] explain why we reconfigure printing all the time
---
tests/proofmode_ascii.v | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/tests/proofmode_ascii.v b/tests/proofmode_ascii.v
index cdefd0d4e..e29a22860 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.
--
GitLab