From 550db27f8c27e03ecc4defc804c8f360af64fbd6 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 27 Mar 2020 18:06:26 +0000
Subject: Update path for newer versions of BBV Coq library

---
 lib/coq/Makefile | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/coq/Makefile b/lib/coq/Makefile
index d16191cb..806b0ff0 100644
--- a/lib/coq/Makefile
+++ b/lib/coq/Makefile
@@ -1,10 +1,10 @@
-BBV_DIR?=../../../bbv
+BBV_DIR?=../../../bbv/src/bbv
 
 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
 SRC=$(CORESRC) $(PROOFSRC)
 
-COQ_LIBS = -R . Sail -R "$(BBV_DIR)/theories" bbv
+COQ_LIBS = -R . Sail -R "$(BBV_DIR)" bbv
 
 TARGETS=$(SRC:.v=.vo)
 
-- 
cgit v1.2.3