diff options
| -rw-r--r-- | lib/coq/Operators.v | 1 | ||||
| -rw-r--r-- | lib/coq/Operators_mwords.v | 2 | ||||
| -rw-r--r-- | lib/coq/Prompt.v | 1 | ||||
| -rw-r--r-- | lib/coq/Prompt_monad.v | 1 | ||||
| -rw-r--r-- | lib/coq/Real.v | 1 | ||||
| -rw-r--r-- | lib/coq/State.v | 1 | ||||
| -rw-r--r-- | lib/coq/State_lemmas.v | 1 | ||||
| -rw-r--r-- | lib/coq/State_monad.v | 1 | ||||
| -rw-r--r-- | lib/coq/String.v | 1 | ||||
| -rw-r--r-- | lib/coq/Values.v | 4 | ||||
| -rw-r--r-- | src/pretty_print_coq.ml | 4 | ||||
| -rwxr-xr-x | test/coq/run_tests.sh | 6 |
12 files changed, 19 insertions, 5 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. 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; diff --git a/test/coq/run_tests.sh b/test/coq/run_tests.sh index c31b1475..2d1a1318 100755 --- a/test/coq/run_tests.sh +++ b/test/coq/run_tests.sh @@ -6,10 +6,12 @@ SAILDIR="$DIR/../.." TYPECHECKTESTSDIR="$DIR/../typecheck/pass" EXTRATESTSDIR="$DIR/pass" -if [ -z "$BBVDIR" ] || opam config var coq-bbv:share >/dev/null 2>/dev/null; then +if opam config var coq-bbv:share >/dev/null 2>/dev/null; then COQOPTS="-Q $SAILDIR/lib/coq Sail" else - BBVDIR="$DIR/../../../bbv/src/bbv" + if [ -z "$BBVDIR" ]; then + BBVDIR="$DIR/../../../bbv/src/bbv" + fi COQOPTS="-Q $SAILDIR/lib/coq Sail -Q $BBVDIR bbv" fi |