Coq: library name update (as we did for Lem)

11 files changed, 19 insertions, 19 deletions

diff --git a/lib/coq/Makefile b/lib/coq/Makefile
index d974b692..816a6c3d 100644
--- a/lib/coq/Makefile
+++ b/lib/coq/Makefile
@@ -1,6 +1,6 @@
 BBV_DIR=../../../bbv
 
-SRC=Prompt_monad.v  Prompt.v  Sail_impl_base.v  Sail_instr_kinds.v  Sail_operators_bitlists.v  Sail_operators_mwords.v  Sail_operators.v  Sail_values.v  State_monad.v  State.v
+SRC=Sail2_prompt_monad.v  Sail2_prompt.v  Sail2_impl_base.v  Sail2_instr_kinds.v  Sail2_operators_bitlists.v  Sail2_operators_mwords.v  Sail2_operators.v  Sail2_values.v  Sail2_state_monad.v  Sail2_state.v
 
 COQ_LIBS = -R . Sail -R "$(BBV_DIR)" bbv
 
diff --git a/lib/coq/Sail_impl_base.v b/lib/coq/Sail2_impl_base.v
index df7854e7..464c2902 100644
--- a/lib/coq/Sail_impl_base.v
+++ b/lib/coq/Sail2_impl_base.v
@@ -48,7 +48,7 @@
 (*  SUCH DAMAGE.                                                          *)
 (*========================================================================*)
 
-Require Import Sail_instr_kinds.
+Require Import Sail2_instr_kinds.
 
 (*
 class ( EnumerationType 'a ) 
diff --git a/lib/coq/Sail_instr_kinds.v b/lib/coq/Sail2_instr_kinds.v
index 57532e92..57532e92 100644
--- a/lib/coq/Sail_instr_kinds.v
+++ b/lib/coq/Sail2_instr_kinds.v
diff --git a/lib/coq/Sail_operators.v b/lib/coq/Sail2_operators.v
index b14cdd85..b2059b93 100644
--- a/lib/coq/Sail_operators.v
+++ b/lib/coq/Sail2_operators.v
@@ -1,4 +1,4 @@
-Require Import Sail_values.
+Require Import Sail2_values.
 Require List.
 
 (*** Bit vector operations *)
diff --git a/lib/coq/Sail_operators_bitlists.v b/lib/coq/Sail2_operators_bitlists.v
index 51c3e972..dbd8215c 100644
--- a/lib/coq/Sail_operators_bitlists.v
+++ b/lib/coq/Sail2_operators_bitlists.v
@@ -1,5 +1,5 @@
-Require Import Sail_values.
-Require Import Sail_operators.
+Require Import Sail2_values.
+Require Import Sail2_operators.
 
 (*
 
diff --git a/lib/coq/Sail_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v
index a962d554..30ed1da0 100644
--- a/lib/coq/Sail_operators_mwords.v
+++ b/lib/coq/Sail2_operators_mwords.v
@@ -1,7 +1,7 @@
-Require Import Sail_values.
-Require Import Sail_operators.
-Require Import Prompt_monad.
-Require Import Prompt.
+Require Import Sail2_values.
+Require Import Sail2_operators.
+Require Import Sail2_prompt_monad.
+Require Import Sail2_prompt.
 Require bbv.Word.
 Require Import Arith.
 Require Import Omega.
diff --git a/lib/coq/Prompt.v b/lib/coq/Sail2_prompt.v
index 122da918..802fc302 100644
--- a/lib/coq/Prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -1,6 +1,6 @@
 (*Require Import Sail_impl_base*)
-Require Import Sail_values.
-Require Import Prompt_monad.
+Require Import Sail2_values.
+Require Import Sail2_prompt_monad.
 
 Require Import List.
 Import ListNotations.
diff --git a/lib/coq/Prompt_monad.v b/lib/coq/Sail2_prompt_monad.v
index 9f413aa3..5bb9d477 100644
--- a/lib/coq/Prompt_monad.v
+++ b/lib/coq/Sail2_prompt_monad.v
@@ -1,7 +1,7 @@
 Require Import String.
 (*Require Import Sail_impl_base*)
-Require Import Sail_instr_kinds.
-Require Import Sail_values.
+Require Import Sail2_instr_kinds.
+Require Import Sail2_values.
 
 
 
diff --git a/lib/coq/State.v b/lib/coq/Sail2_state.v
index 00dd1f5b..7e10aba3 100644
--- a/lib/coq/State.v
+++ b/lib/coq/Sail2_state.v
@@ -1,8 +1,8 @@
 (*Require Import Sail_impl_base*)
-Require Import Sail_values.
-Require Import Prompt_monad.
-Require Import Prompt.
-Require Import State_monad.
+Require Import Sail2_values.
+Require Import Sail2_prompt_monad.
+Require Import Sail2_prompt.
+Require Import Sail2_state_monad.
 (*
 (* State monad wrapper around prompt monad *)
 
diff --git a/lib/coq/State_monad.v b/lib/coq/Sail2_state_monad.v
index f93606e8..c48db31b 100644
--- a/lib/coq/State_monad.v
+++ b/lib/coq/Sail2_state_monad.v
@@ -1,5 +1,5 @@
-Require Import Sail_instr_kinds.
-Require Import Sail_values.
+Require Import Sail2_instr_kinds.
+Require Import Sail2_values.
 (*
 (* 'a is result type *)
 
diff --git a/lib/coq/Sail_values.v b/lib/coq/Sail2_values.v
index c211cfdc..c211cfdc 100644
--- a/lib/coq/Sail_values.v
+++ b/lib/coq/Sail2_values.v