20 files changed, 90 insertions, 71 deletions
diff --git a/lib/coq/Base.v b/lib/coq/Base.v
new file mode 100644
index 00000000..1807d151
--- /dev/null
+++ b/lib/coq/Base.v
@@ -0,0 +1,7 @@
+Require Export Sail.Instr_kinds.
+Require Export Sail.Values.
+Require Export Sail.String.
+Require Export Sail.Operators_mwords.
+Require Export Sail.Prompt_monad.
+Require Export Sail.Prompt.
+Require Export Sail.State.
diff --git a/lib/coq/Hoare.v b/lib/coq/Hoare.v
index f5d764b2..b883b7a7 100644
--- a/lib/coq/Hoare.v
+++ b/lib/coq/Hoare.v
@@ -1,6 +1,6 @@
 Require Import String ZArith Setoid Morphisms Equivalence.
-Require Import Sail2_state_monad Sail2_prompt Sail2_state Sail2_state_monad_lemmas.
-Require Import Sail2_state_lemmas.
+Require Import Sail.State_monad Sail.Prompt Sail.State Sail.State_monad_lemmas.
+Require Import Sail.State_lemmas.
 
 (*adhoc_overloading
   Monad_Syntax.bind State_monad.bindS*)
@@ -193,9 +193,9 @@ eapply PrePost_bindS.
 Qed.
 
 Lemma PrePost_and_boolSP (*[PrePost_compositeI]:*) Regs E PP QQ RR H
-  (l : monadS Regs {b : bool & Sail2_values.ArithFactP (PP b)} E)
-  (r : monadS Regs {b : bool & Sail2_values.ArithFactP (QQ b)} E)
-  P (Q : result {b : bool & Sail2_values.ArithFactP (RR b)} E -> predS Regs) R :
+  (l : monadS Regs {b : bool & Sail.Values.ArithFactP (PP b)} E)
+  (r : monadS Regs {b : bool & Sail.Values.ArithFactP (QQ b)} E)
+  P (Q : result {b : bool & Sail.Values.ArithFactP (RR b)} E -> predS Regs) R :
   (forall p,
       PrePost R r
               (fun r =>
@@ -237,9 +237,9 @@ eapply PrePost_bindS.
 Qed.
 
 Lemma PrePost_or_boolSP (*[PrePost_compositeI]:*) Regs E PP QQ RR H
-  (l : monadS Regs {b : bool & Sail2_values.ArithFactP (PP b)} E)
-  (r : monadS Regs {b : bool & Sail2_values.ArithFactP (QQ b)} E)
-  P (Q : result {b : bool & Sail2_values.ArithFactP (RR b)} E -> predS Regs) R :
+  (l : monadS Regs {b : bool & Sail.Values.ArithFactP (PP b)} E)
+  (r : monadS Regs {b : bool & Sail.Values.ArithFactP (QQ b)} E)
+  P (Q : result {b : bool & Sail.Values.ArithFactP (RR b)} E -> predS Regs) R :
   (forall p,
       PrePost R r
               (fun r =>
@@ -608,9 +608,9 @@ Qed.
    and prevents the reduction of the function application. *)
 
 Lemma PrePostE_and_boolSP (*[PrePost_compositeI]:*) Regs Ety PP QQ RR H
-  (l : monadS Regs {b : bool & Sail2_values.ArithFactP (PP b)} Ety)
-  (r : monadS Regs {b : bool & Sail2_values.ArithFactP (QQ b)} Ety)
-  P (Q : {b : bool & Sail2_values.ArithFactP (RR b)} -> predS Regs) E R :
+  (l : monadS Regs {b : bool & Sail.Values.ArithFactP (PP b)} Ety)
+  (r : monadS Regs {b : bool & Sail.Values.ArithFactP (QQ b)} Ety)
+  P (Q : {b : bool & Sail.Values.ArithFactP (RR b)} -> predS Regs) E R :
   PrePostE R r (fun r s => forall pf, Q (existT _ (projT1 r) pf) s) E ->
   PrePostE P l
           (fun r s => match r with
@@ -645,9 +645,9 @@ eapply PrePostE_bindS.
 Qed.
 
 Lemma PrePostE_or_boolSP (*[PrePost_compositeI]:*) Regs Ety PP QQ RR H
-  (l : monadS Regs {b : bool & Sail2_values.ArithFactP (PP b)} Ety)
-  (r : monadS Regs {b : bool & Sail2_values.ArithFactP (QQ b)} Ety)
-  P (Q : {b : bool & Sail2_values.ArithFactP (RR b)} -> predS Regs) E R :
+  (l : monadS Regs {b : bool & Sail.Values.ArithFactP (PP b)} Ety)
+  (r : monadS Regs {b : bool & Sail.Values.ArithFactP (QQ b)} Ety)
+  P (Q : {b : bool & Sail.Values.ArithFactP (RR b)} -> predS Regs) E R :
   PrePostE R r (fun r s => forall pf, Q (existT _ (projT1 r) pf) s) E ->
   PrePostE P l
           (fun r s => match r with
@@ -774,7 +774,7 @@ apply PrePost_foreachS_invariant with (Q := fun v => match v with Value a => Q a
 auto.
 Qed.
 
-Lemma PrePostE_foreach_ZS_up_invariant Regs Vars Ety from to step (H : Sail2_values.ArithFact (0 <? step)%Z) vars body (Q : Vars -> predS Regs) (E : ex Ety -> predS Regs) :
+Lemma PrePostE_foreach_ZS_up_invariant Regs Vars Ety from to step (H : Sail.Values.ArithFact (0 <? step)%Z) vars body (Q : Vars -> predS Regs) (E : ex Ety -> predS Regs) :
   (forall i range vars, PrePostE (Q vars) (body i range vars) Q E) ->
   PrePostE (Q vars) (foreach_ZS_up from to step vars body) Q E.
 intro INV.
@@ -793,7 +793,7 @@ induction (S (Z.abs_nat (from - to))); intros.
   + apply PrePostE_returnS.
 Qed.
 
-Lemma PrePostE_foreach_ZS_down_invariant Regs Vars Ety from to step (H : Sail2_values.ArithFact (0 <? step)%Z) vars body (Q : Vars -> predS Regs) (E : ex Ety -> predS Regs) :
+Lemma PrePostE_foreach_ZS_down_invariant Regs Vars Ety from to step (H : Sail.Values.ArithFact (0 <? step)%Z) vars body (Q : Vars -> predS Regs) (E : ex Ety -> predS Regs) :
   (forall i range vars, PrePostE (Q vars) (body i range vars) Q E) ->
   PrePostE (Q vars) (foreach_ZS_down from to step vars body) Q E.
 intro INV.
@@ -838,7 +838,7 @@ apply PrePostE_use_pre. intros s0 Pre0.
 assert (measure vars >= 0) as Hlimit_0 by eauto. clear s0 Pre0.
 remember (measure vars) as limit eqn: Heqlimit in Hlimit_0 |- *.
 assert (measure vars <= limit) as Hlimit by omega. clear Heqlimit.
-generalize (Sail2_prompt.Zwf_guarded limit).
+generalize (Sail.Prompt.Zwf_guarded limit).
 revert vars Hlimit.
 apply Wf_Z.natlike_ind with (x := limit).
 * intros vars Hmeasure_limit [acc]. simpl.
@@ -1000,7 +1000,7 @@ unfold internal_pickS.
 intro notnil.
 eapply PrePostE_bindS with (R := fun _ s => forall x, List.In x xs -> Q x s).
 * intros.
-  destruct (nth_error_modulo (Sail2_values.nat_of_bools a) notnil) as (x & IN & nth).
+  destruct (nth_error_modulo (Sail.Values.nat_of_bools a) notnil) as (x & IN & nth).
   rewrite nth.
   eapply PrePostE_strengthen_pre.
   apply PrePostE_returnS.
@@ -1038,7 +1038,7 @@ Qed.
 
 Local Open Scope Z.
 
-Lemma PrePostE_undefined_bitvectorS_any Regs Ety n `{Sail2_values.ArithFact (n >=? 0)} (Q : Sail2_values.mword n -> predS Regs) (E : ex Ety -> predS Regs) :
+Lemma PrePostE_undefined_bitvectorS_any Regs Ety n `{Sail.Values.ArithFact (n >=? 0)} (Q : Sail.Values.mword n -> predS Regs) (E : ex Ety -> predS Regs) :
   PrePostE (fun s => forall w, Q w s) (undefined_bitvectorS n) Q E.
 unfold undefined_bitvectorS.
 eapply PrePostE_strengthen_pre.
@@ -1049,15 +1049,15 @@ simpl.
 auto.
 Qed.
 
-Lemma PrePostE_undefined_bitvectorS_ignore Regs Ety n `{Sail2_values.ArithFact (n >=? 0)} (Q : predS Regs) (E : ex Ety -> predS Regs) :
+Lemma PrePostE_undefined_bitvectorS_ignore Regs Ety n `{Sail.Values.ArithFact (n >=? 0)} (Q : predS Regs) (E : ex Ety -> predS Regs) :
   PrePostE Q (undefined_bitvectorS n) (fun _ => Q) E.
 eapply PrePostE_strengthen_pre.
 apply PrePostE_undefined_bitvectorS_any; auto.
 simpl; auto.
 Qed.
 
-Lemma PrePostE_build_trivial_exS Regs (T:Type) Ety (m : monadS Regs T Ety) P (Q : {T & Sail2_values.ArithFact true} -> predS Regs) E :
-  PrePostE P m (fun v => Q (existT _ v (Sail2_values.Build_ArithFactP _ eq_refl))) E ->
+Lemma PrePostE_build_trivial_exS Regs (T:Type) Ety (m : monadS Regs T Ety) P (Q : {T & Sail.Values.ArithFact true} -> predS Regs) E :
+  PrePostE P m (fun v => Q (existT _ v (Sail.Values.Build_ArithFactP _ eq_refl))) E ->
   PrePostE P (build_trivial_exS m) Q E.
 intro H.
 unfold build_trivial_exS.
diff --git a/lib/coq/Sail2_impl_base.v b/lib/coq/Impl_base.v
index 464c2902..b5a2dd54 100644
--- a/lib/coq/Sail2_impl_base.v
+++ b/lib/coq/Impl_base.v
@@ -48,7 +48,7 @@
 (*  SUCH DAMAGE.                                                          *)
 (*========================================================================*)
 
-Require Import Sail2_instr_kinds.
+Require Import Sail.Instr_kinds.
 
 (*
 class ( EnumerationType 'a ) 
diff --git a/lib/coq/Sail2_instr_kinds.v b/lib/coq/Instr_kinds.v
index d03d5e63..d03d5e63 100644
--- a/lib/coq/Sail2_instr_kinds.v
+++ b/lib/coq/Instr_kinds.v
diff --git a/lib/coq/Makefile b/lib/coq/Makefile
index 806b0ff0..1b6435e1 100644
--- a/lib/coq/Makefile
+++ b/lib/coq/Makefile
@@ -1,26 +1,40 @@
+HAVE_OPAM_BBV=$(shell if opam config var coq-bbv:share >/dev/null 2>/dev/null; then echo yes; else echo no; fi)
+
+ifeq ($(HAVE_OPAM_BBV),no)
 BBV_DIR?=../../../bbv/src/bbv
+endif
 
-CORESRC=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  Sail2_state_lifting.v  Sail2_string.v  Sail2_real.v
-PROOFSRC=Sail2_values_lemmas.v Sail2_state_monad_lemmas.v Sail2_state_lemmas.v Hoare.v
+CORESRC=Prompt_monad.v  Prompt.v  Impl_base.v  Instr_kinds.v  Operators_bitlists.v  Operators_mwords.v  Operators.v  Values.v  State_monad.v  State.v  State_lifting.v  String.v  Real.v  Base.v
+PROOFSRC=Values_lemmas.v State_monad_lemmas.v State_lemmas.v Hoare.v
 SRC=$(CORESRC) $(PROOFSRC)
 
-COQ_LIBS = -R . Sail -R "$(BBV_DIR)" bbv
+ifdef BBV_DIR
+COQ_LIBS = -Q . Sail -Q "$(BBV_DIR)" bbv
+else
+COQ_LIBS = -Q . Sail
+endif
 
 TARGETS=$(SRC:.v=.vo)
 
-.PHONY: all clean *.ide
+.PHONY: all clean install
 
 all: $(TARGETS)
 clean:
 	rm -f -- $(TARGETS) $(TARGETS:.vo=.glob) $(TARGETS:%.vo=.%.aux) deps
 
-%.vo: %.v
+$(TARGETS): %.vo: %.v
 	coqc $(COQ_LIBS) $<
 
-%.ide: %.v
-	coqide $(COQ_LIBS) $<
-
 deps: $(SRC)
 	coqdep $(COQ_LIBS) $(SRC) > deps
 
 -include deps
+
+COQLIB = $(shell coqc -where)
+DESTDIR ?=
+INSTALLDIR = $(DESTDIR)/$(COQLIB)/user-contrib/Sail
+
+install: $(TARGETS)
+	test -d "$(DESTDIR)/$(COQLIB)/user-contrib" || echo Coq library directory "$(DESTDIR)/$(COQLIB)/user-contrib" not present
+	install -d -- "$(INSTALLDIR)"
+	install -m 644 -- $(SRC) $(TARGETS) $(TARGETS:.vo=.glob) "$(INSTALLDIR)"
diff --git a/lib/coq/Sail2_operators.v b/lib/coq/Operators.v
index ab02c4a8..fa5377ce 100644
--- a/lib/coq/Sail2_operators.v
+++ b/lib/coq/Operators.v
@@ -1,4 +1,4 @@
-Require Import Sail2_values.
+Require Import Sail.Values.
 Require List.
 Import List.ListNotations.
 
diff --git a/lib/coq/Sail2_operators_bitlists.v b/lib/coq/Operators_bitlists.v
index dbd8215c..85a01bf9 100644
--- a/lib/coq/Sail2_operators_bitlists.v
+++ b/lib/coq/Operators_bitlists.v
@@ -1,5 +1,5 @@
-Require Import Sail2_values.
-Require Import Sail2_operators.
+Require Import Sail.Values.
+Require Import Sail.Operators.
 
 (*
 
diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Operators_mwords.v
index 1f176ad9..c4acd69d 100644
--- a/lib/coq/Sail2_operators_mwords.v
+++ b/lib/coq/Operators_mwords.v
@@ -1,7 +1,7 @@
-Require Import Sail2_values.
-Require Import Sail2_operators.
-Require Import Sail2_prompt_monad.
-Require Import Sail2_prompt.
+Require Import Sail.Values.
+Require Import Sail.Operators.
+Require Import Sail.Prompt_monad.
+Require Import Sail.Prompt.
 Require Import bbv.Word.
 Require bbv.BinNotation.
 Require Import Arith.
diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Prompt.v
index aeca1248..5a82acdc 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Prompt.v
@@ -1,6 +1,5 @@
-(*Require Import Sail_impl_base*)
-Require Import Sail2_values.
-Require Import Sail2_prompt_monad.
+Require Import Sail.Values.
+Require Import Sail.Prompt_monad.
 Require Export ZArith.Zwf.
 Require Import List.
 Import ListNotations.
diff --git a/lib/coq/Sail2_prompt_monad.v b/lib/coq/Prompt_monad.v
index 0ff65d28..5f54ad0d 100644
--- a/lib/coq/Sail2_prompt_monad.v
+++ b/lib/coq/Prompt_monad.v
@@ -1,7 +1,7 @@
 Require Import String.
 (*Require Import Sail_impl_base*)
-Require Import Sail2_instr_kinds.
-Require Import Sail2_values.
+Require Import Sail.Instr_kinds.
+Require Import Sail.Values.
 Require bbv.Word.
 Import ListNotations.
 
diff --git a/lib/coq/Sail2_real.v b/lib/coq/Real.v
index 4800f18b..3a3f3a2f 100644
--- a/lib/coq/Sail2_real.v
+++ b/lib/coq/Real.v
@@ -1,7 +1,7 @@
 Require Export Rbase.
 Require Import Reals.
 Require Export ROrderedType.
-Require Import Sail2_values.
+Require Import Sail.Values.
 
 (* "Decidable" in a classical sense... *)
 Instance Decidable_eq_real : forall (x y : R), Decidable (x = y) :=
diff --git a/lib/coq/Sail2_state.v b/lib/coq/State.v
index 7c751bc7..f4e5c266 100644
--- a/lib/coq/Sail2_state.v
+++ b/lib/coq/State.v
@@ -1,8 +1,7 @@
-(*Require Import Sail_impl_base*)
-Require Import Sail2_values.
-Require Import Sail2_prompt_monad.
-Require Import Sail2_prompt.
-Require Import Sail2_state_monad.
+Require Import Sail.Values.
+Require Import Sail.Prompt_monad.
+Require Import Sail.Prompt.
+Require Import Sail.State_monad.
 Import ListNotations.
 
 (*val iterS_aux : forall 'rv 'a 'e. integer -> (integer -> 'a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e*)
diff --git a/lib/coq/Sail2_state_lemmas.v b/lib/coq/State_lemmas.v
index ef82084f..78a7d1de 100644
--- a/lib/coq/Sail2_state_lemmas.v
+++ b/lib/coq/State_lemmas.v
@@ -1,5 +1,5 @@
-Require Import Sail2_values Sail2_prompt_monad Sail2_prompt Sail2_state_monad Sail2_state Sail2_state Sail2_state_lifting.
-Require Import Sail2_state_monad_lemmas.
+Require Import Sail.Values Sail.Prompt_monad Sail.Prompt Sail.State_monad Sail.State Sail.State Sail.State_lifting.
+Require Import Sail.State_monad_lemmas.
 
 Local Open Scope equiv_scope.
 
@@ -209,14 +209,14 @@ Qed.
 
 (* Monad lifting *)
 
-Lemma liftState_bind Regval Regs A B E {r : Sail2_values.register_accessors Regs Regval} {m : monad Regval A E} {f : A -> monad Regval B E} :
+Lemma liftState_bind Regval Regs A B E {r : Sail.Values.register_accessors Regs Regval} {m : monad Regval A E} {f : A -> monad Regval B E} :
   liftState r (bind m f) === bindS (liftState r m) (fun x => liftState r (f x)).
 induction m; simpl; autorewrite with state; auto using bindS_cong.
 Qed.
 Hint Rewrite liftState_bind : liftState.
 Hint Resolve liftState_bind : liftState.
 
-Lemma liftState_bind0 Regval Regs B E {r : Sail2_values.register_accessors Regs Regval} {m : monad Regval unit E} {m' : monad Regval B E} :
+Lemma liftState_bind0 Regval Regs B E {r : Sail.Values.register_accessors Regs Regval} {m : monad Regval unit E} {m' : monad Regval B E} :
   liftState r (bind0 m m') === seqS (liftState r m) (liftState r m').
 induction m; simpl; autorewrite with state; auto using bindS_cong.
 Qed.
@@ -327,7 +327,7 @@ Ltac rewrite_liftState :=
     try let H := fresh "H" in (eassert (H:liftState r tm === _); [ statecong liftState | rewrite H; clear H])
   end.
 
-Lemma liftState_return Regval Regs A E {r : Sail2_values.register_accessors Regs Regval} {a :A} :
+Lemma liftState_return Regval Regs A E {r : Sail.Values.register_accessors Regs Regval} {a :A} :
   liftState (E:=E) r (returnm a) = returnS a.
 reflexivity.
 Qed.
@@ -633,7 +633,7 @@ Hint Resolve liftState_write_mem_ea : liftState.
 Lemma liftState_write_memt Regs Regval A B E wk addr sz v t r :
   liftState (Regs := Regs) r (@write_memt Regval A B E wk addr sz v t) = write_memtS wk addr sz v t.
 unfold write_memt, write_memtS.
-destruct (Sail2_values.mem_bytes_of_bits v); auto.
+destruct (Sail.Values.mem_bytes_of_bits v); auto.
 Qed.
 Hint Rewrite liftState_write_memt : liftState.
 Hint Resolve liftState_write_memt : liftState.
@@ -641,7 +641,7 @@ Hint Resolve liftState_write_memt : liftState.
 Lemma liftState_write_mem Regs Regval A B E wk addrsize addr sz v r :
   liftState (Regs := Regs) r (@write_mem Regval A B E wk addrsize addr sz v) = write_memS wk addr sz v.
 unfold write_mem, write_memS, write_memtS.
-destruct (Sail2_values.mem_bytes_of_bits v); simpl; auto.
+destruct (Sail.Values.mem_bytes_of_bits v); simpl; auto.
 Qed.
 Hint Rewrite liftState_write_mem : liftState.
 Hint Resolve liftState_write_mem : liftState.
diff --git a/lib/coq/Sail2_state_lifting.v b/lib/coq/State_lifting.v
index 1544c3c9..8342b04c 100644
--- a/lib/coq/Sail2_state_lifting.v
+++ b/lib/coq/State_lifting.v
@@ -1,7 +1,7 @@
-Require Import Sail2_values.
-Require Import Sail2_prompt_monad.
-Require Import Sail2_prompt.
-Require Import Sail2_state_monad.
+Require Import Sail.Values.
+Require Import Sail.Prompt_monad.
+Require Import Sail.Prompt.
+Require Import Sail.State_monad.
 Import ListNotations.
 
 (* Lifting from prompt monad to state monad *)
diff --git a/lib/coq/Sail2_state_monad.v b/lib/coq/State_monad.v
index 3fb1f8d9..38f942ee 100644
--- a/lib/coq/Sail2_state_monad.v
+++ b/lib/coq/State_monad.v
@@ -1,5 +1,5 @@
-Require Import Sail2_instr_kinds.
-Require Import Sail2_values.
+Require Import Sail.Instr_kinds.
+Require Import Sail.Values.
 Require FMapList.
 Require Import OrderedType.
 Require OrderedTypeEx.
diff --git a/lib/coq/Sail2_state_monad_lemmas.v b/lib/coq/State_monad_lemmas.v
index c834a0cb..41270be6 100644
--- a/lib/coq/Sail2_state_monad_lemmas.v
+++ b/lib/coq/State_monad_lemmas.v
@@ -1,5 +1,5 @@
-Require Import Sail2_state_monad.
-(*Require Import Sail2_values_lemmas.*)
+Require Import Sail.State_monad.
+(*Require Import Sail.Values_lemmas.*)
 Require Export Setoid.
 Require Export Morphisms Equivalence.
 
@@ -8,7 +8,7 @@ Require Export Morphisms Equivalence.
    Note that rewriting results are put into both a rewriting hint database and
    a normal automation one.  The former can be used with autorewrite and friends,
    but the latter can be used with the rewriting under congruence tactics, such as
-   statecong in Sail2_state_lemmas, and PrePostE_rewrite in Hoare. *)
+   statecong in Sail.State_lemmas, and PrePostE_rewrite in Hoare. *)
 
 (* Ensure that pointwise equality on states is the preferred notion of
    equivalence for the state monad. *)
@@ -540,7 +540,7 @@ Hint Resolve no_throw_mem_builtins_7 : ignore_throw.
 Lemma no_throw_mem_builtins_8 Regs E1 E2 A B wk addr sz v t :
   ignore_throw (E2 := E2) (@write_memtS Regs E1 A B wk addr sz v t) === write_memtS wk addr sz v t.
 unfold write_memtS. rewrite ignore_throw_option_case_distrib_2.
-destruct (Sail2_values.mem_bytes_of_bits v); autorewrite with ignore_throw; auto.
+destruct (Sail.Values.mem_bytes_of_bits v); autorewrite with ignore_throw; auto.
 Qed.
 Hint Rewrite no_throw_mem_builtins_8 : ignore_throw.
 Hint Resolve no_throw_mem_builtins_8 : ignore_throw.
diff --git a/lib/coq/Sail2_string.v b/lib/coq/String.v
index 1e1b445b..207aac5f 100644
--- a/lib/coq/Sail2_string.v
+++ b/lib/coq/String.v
@@ -1,4 +1,4 @@
-Require Import Sail2_values.
+Require Import Sail.Values.
 Require Import Coq.Strings.Ascii.
 
 Definition string_sub (s : string) (start : Z) (len : Z) : string :=
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Values.v
index 9b76ce62..9b76ce62 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Values.v
diff --git a/lib/coq/Sail2_values_lemmas.v b/lib/coq/Values_lemmas.v
index ed8b6af0..8444937f 100644
--- a/lib/coq/Sail2_values_lemmas.v
+++ b/lib/coq/Values_lemmas.v
@@ -1,4 +1,4 @@
-Require Import Sail2_values.
+Require Import Sail.Values.
 
 (*
 
@@ -389,4 +389,4 @@ lemma bools_of_int_bin_to_bl[simp]:
   by (auto simp: bools_of_int_def Let_def map_Not_bin_to_bl rbl_succ[unfolded bin_to_bl_def])
 
 end
-*)
-\ No newline at end of file
+*)
diff --git a/lib/coq/_CoqProject b/lib/coq/_CoqProject
index 9f5d26b8..fbefc692 100644
--- a/lib/coq/_CoqProject
+++ b/lib/coq/_CoqProject
@@ -1,2 +1,2 @@
--R . Sail
--R ../../../bbv/theories bbv
+-Q . Sail
+-Q ../../../bbv/theories bbv