Coq: tidy up scope in library

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

10 files changed, 11 insertions, 3 deletions

diff --git a/lib/coq/Operators.v b/lib/coq/Operators.v
index fa5377ce..2f12eac7 100644
--- a/lib/coq/Operators.v
+++ b/lib/coq/Operators.v
@@ -1,6 +1,7 @@
 Require Import Sail.Values.
 Require List.
 Import List.ListNotations.
+Local Open Scope Z.
 
 (*** Bit vector operations *)
 
diff --git a/lib/coq/Operators_mwords.v b/lib/coq/Operators_mwords.v
index c4acd69d..ccb3b1de 100644
--- a/lib/coq/Operators_mwords.v
+++ b/lib/coq/Operators_mwords.v
@@ -8,7 +8,7 @@ Require Import Arith.
 Require Import ZArith.
 Require Import Omega.
 Require Import Eqdep_dec.
-Open Scope Z.
+Local Open Scope Z.
 
 Fixpoint cast_positive (T : positive -> Type) (p q : positive) : T p -> p = q -> T q.
 refine (
diff --git a/lib/coq/Prompt.v b/lib/coq/Prompt.v
index 5a82acdc..718b2f47 100644
--- a/lib/coq/Prompt.v
+++ b/lib/coq/Prompt.v
@@ -3,6 +3,7 @@ Require Import Sail.Prompt_monad.
 Require Export ZArith.Zwf.
 Require Import List.
 Import ListNotations.
+Local Open Scope Z.
 (*
 
 val iter_aux : forall 'rv 'a 'e. integer -> (integer -> 'a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e
diff --git a/lib/coq/Prompt_monad.v b/lib/coq/Prompt_monad.v
index 5f54ad0d..ddd40cd0 100644
--- a/lib/coq/Prompt_monad.v
+++ b/lib/coq/Prompt_monad.v
@@ -4,6 +4,7 @@ Require Import Sail.Instr_kinds.
 Require Import Sail.Values.
 Require bbv.Word.
 Import ListNotations.
+Local Open Scope Z.
 
 Definition register_name := string.
 Definition address := list bitU.
diff --git a/lib/coq/Real.v b/lib/coq/Real.v
index 3a3f3a2f..a2da0e71 100644
--- a/lib/coq/Real.v
+++ b/lib/coq/Real.v
@@ -2,6 +2,7 @@ Require Export Rbase.
 Require Import Reals.
 Require Export ROrderedType.
 Require Import Sail.Values.
+Local Open Scope Z.
 
 (* "Decidable" in a classical sense... *)
 Instance Decidable_eq_real : forall (x y : R), Decidable (x = y) :=
diff --git a/lib/coq/State.v b/lib/coq/State.v
index f4e5c266..a0b2113d 100644
--- a/lib/coq/State.v
+++ b/lib/coq/State.v
@@ -3,6 +3,7 @@ Require Import Sail.Prompt_monad.
 Require Import Sail.Prompt.
 Require Import Sail.State_monad.
 Import ListNotations.
+Local Open Scope Z.
 
 (*val iterS_aux : forall 'rv 'a 'e. integer -> (integer -> 'a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e*)
 Fixpoint iterS_aux {RV A E} i (f : Z -> A -> monadS RV unit E) (xs : list A) :=
diff --git a/lib/coq/State_lemmas.v b/lib/coq/State_lemmas.v
index 78a7d1de..6a620f27 100644
--- a/lib/coq/State_lemmas.v
+++ b/lib/coq/State_lemmas.v
@@ -2,6 +2,7 @@ Require Import Sail.Values Sail.Prompt_monad Sail.Prompt Sail.State_monad Sail.S
 Require Import Sail.State_monad_lemmas.
 
 Local Open Scope equiv_scope.
+Local Open Scope Z.
 
 Lemma seqS_cong A RV E (m1 m1' : monadS RV unit E) (m2 m2' : monadS RV A E) :
   m1 === m1' ->
diff --git a/lib/coq/State_monad.v b/lib/coq/State_monad.v
index 38f942ee..fb68bd39 100644
--- a/lib/coq/State_monad.v
+++ b/lib/coq/State_monad.v
@@ -6,6 +6,7 @@ Require OrderedTypeEx.
 Require Import List.
 Require bbv.Word.
 Import ListNotations.
+Local Open Scope Z.
 
 (* TODO: revisit choice of FMapList *)
 Module NatMap := FMapList.Make(OrderedTypeEx.Nat_as_OT).
diff --git a/lib/coq/String.v b/lib/coq/String.v
index 207aac5f..5b4e120d 100644
--- a/lib/coq/String.v
+++ b/lib/coq/String.v
@@ -1,5 +1,6 @@
 Require Import Sail.Values.
 Require Import Coq.Strings.Ascii.
+Local Open Scope Z.
 
 Definition string_sub (s : string) (start : Z) (len : Z) : string :=
   String.substring (Z.to_nat start) (Z.to_nat len) s.
diff --git a/lib/coq/Values.v b/lib/coq/Values.v
index 256d7c19..1a9eb644 100644
--- a/lib/coq/Values.v
+++ b/lib/coq/Values.v
@@ -14,8 +14,8 @@ Require Export Zeuclid.
 Require Import Lia.
 Import ListNotations.
 
-Open Scope Z.
-Open Scope bool.
+Local Open Scope Z.
+Local Open Scope bool.
 
 Module Z_eq_dec.
 Definition U := Z.