From e22bb9841a5186d0b52b8fa9ad8cf2e46fa51d76 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Sun, 14 Jun 2020 22:27:30 +0100
Subject: Coq: tidy up scope in library Helps with Coq 8.11.  Also fix BBVDIR
 default in test script.

---
 src/pretty_print_coq.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 17dba718..d0d13907 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -3311,6 +3311,10 @@ try
           (fun lib -> separate space [string "Require Import";string lib] ^^ dot) types_modules;hardline;
         string "Import ListNotations.";
         hardline;
+        string "Open Scope string."; hardline;
+        string "Open Scope bool."; hardline;
+        string "Open Scope Z."; hardline;
+        hardline;
         separate empty (List.map doc_def typdefs); hardline;
         hardline;
         separate empty (List.map doc_def statedefs); hardline;
-- 
cgit v1.2.3