Coq: tidy up scope in library

Helps with Coq 8.11.  Also fix BBVDIR default in test script.

1 files changed, 4 insertions, 0 deletions

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;