From 163f4a4e4467f64759dfa67bd555e6b893692561 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 10 Mar 2022 14:13:19 +0100
Subject: Compile under the name: kvx

---
 Makefile            | 8 ++++----
 lib/Floats.v        | 2 +-
 lib/IEEE754_extra.v | 2 +-
 verilog/Archi.v     | 2 +-
 4 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/Makefile b/Makefile
index 05e4cbcd..412fa775 100644
--- a/Makefile
+++ b/Makefile
@@ -36,18 +36,18 @@ DIRS := lib lib/Impure common $(ARCHDIRS) scheduling backend cfrontend driver \
 RECDIRS:=lib common $(ARCHDIRS) scheduling backend cfrontend driver flocq exportclight \
   cparser
 
-COQINCLUDES := $(foreach d, $(DIRS), -R $(d) compcert.$(subst /,.,$d))
+COQINCLUDES := $(foreach d, $(DIRS), -R $(d) kvx.$(subst /,.,$d))
 
 ifeq ($(LIBRARY_FLOCQ),local)
 DIRS += flocq/Core flocq/Prop flocq/Calc flocq/IEEE754
 RECDIRS += flocq
-COQINCLUDES += -R flocq Flocq
+COQINCLUDES += -R flocq kvx.Flocq
 endif
 
 ifeq ($(LIBRARY_MENHIRLIB),local)
 DIRS += MenhirLib
 RECDIRS += MenhirLib
-COQINCLUDES += -R MenhirLib MenhirLib
+COQINCLUDES += -R MenhirLib kvx.MenhirLib
 endif
 
 # Notes on silenced Coq warnings:
@@ -402,7 +402,7 @@ check-admitted: $(FILES)
 	@grep -w 'admit\|Admitted\|ADMITTED' $^ || echo "Nothing admitted."
 
 check-proof: $(FILES)
-	$(COQCHK) compcert.driver.Complements
+	$(COQCHK) kvx.driver.Complements
 
 print-includes:
 	@echo $(COQINCLUDES)
diff --git a/lib/Floats.v b/lib/Floats.v
index b10b3392..6530b41c 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -18,7 +18,7 @@
 (** Formalization of floating-point numbers, using the Flocq library. *)
 
 Require Import Coqlib Zbits Integers Axioms.
-From Flocq Require Import Binary Bits Core.
+From kvx.Flocq Require Import Binary Bits Core.
 Require Import IEEE754_extra.
 Require Import Program.
 Require Archi.
diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
index b0d1944e..fbcd527e 100644
--- a/lib/IEEE754_extra.v
+++ b/lib/IEEE754_extra.v
@@ -18,7 +18,7 @@
 (** Additional operations and proofs about IEEE-754 binary
     floating-point numbers, on top of the Flocq library. *)
 
-From Flocq Require Import Core Digits Operations Round Bracket Sterbenz
+From kvx.Flocq Require Import Core Digits Operations Round Bracket Sterbenz
                           Binary Round_odd.
 Require Import Psatz.
 Require Import Bool.
diff --git a/verilog/Archi.v b/verilog/Archi.v
index dc5a078d..aef813a4 100644
--- a/verilog/Archi.v
+++ b/verilog/Archi.v
@@ -17,7 +17,7 @@
 
 (** Architecture-dependent parameters for x86 in 32-bit mode *)
 
-From Flocq Require Import Binary Bits.
+From kvx.Flocq Require Import Binary Bits.
 Require Import ZArith List.
 
 Definition ptr64 := false.
-- 
cgit