summaryrefslogtreecommitdiff
path: root/mips/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'mips/Makefile')
-rw-r--r--mips/Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/mips/Makefile b/mips/Makefile
index f8b7588f..062ccd8b 100644
--- a/mips/Makefile
+++ b/mips/Makefile
@@ -48,7 +48,7 @@ mips.v: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS)
mips_types.v: mips.v
MIPS_COQ = mips_types.v mips_extras.v mips.v
-COQ_LIBS = -R ../../bbv bbv -R ../lib/coq Sail
+COQ_LIBS = -R ../../bbv/theories bbv -R ../lib/coq Sail
%.vo: %.v
coqc $(COQ_LIBS) $<