starting to move common files

19 files changed, 5 insertions, 4 deletions

diff --git a/Makefile b/Makefile
index ba8add27..baccc9ab 100644
--- a/Makefile
+++ b/Makefile
@@ -23,7 +23,7 @@ endif
 
 BACKENDLIB?=Asmgenproof0.v Asmgenproof1.v
 
-DIRS=lib common $(ARCHDIRS) backend cfrontend driver \
+DIRS=lib lib/Impure common $(ARCHDIRS) backend cfrontend driver \
   flocq/Core flocq/Prop flocq/Calc flocq/IEEE754 \
   exportclight MenhirLib cparser
 
diff --git a/Makefile.extr b/Makefile.extr
index 59cc6c1d..5e328a4c 100644
--- a/Makefile.extr
+++ b/Makefile.extr
@@ -43,7 +43,7 @@ cparser/pre_parser_messages.ml:
 
 DIRS=extraction \
   lib common $(ARCH) backend cfrontend cparser driver \
-  exportclight debug kvx/unittest kvx/abstractbb/Impure/ocaml \
+  exportclight debug kvx/unittest lib/Impure/ocaml \
   kvx/lib
 
 INCLUDES=$(patsubst %,-I %, $(DIRS))
diff --git a/configure b/configure
index 1eff6d1c..8261f9f3 100755
--- a/configure
+++ b/configure
@@ -694,7 +694,8 @@ echo "-R lib compcert.lib \
 -R flocq compcert.flocq \
 -R exportclight compcert.exportclight \
 -R cparser compcert.cparser \
--R MenhirLib compcert.MenhirLib" > _CoqProject
+-R MenhirLib compcert.MenhirLib
+-R Impure lib.Impure" > _CoqProject
 case $arch in
     x86)
         echo "-R x86_${bitsize} compcert.x86_${bitsize}" >> _CoqProject
@@ -840,7 +841,7 @@ fi
 
 if [ "$arch" = "kvx" ]; then
 cat >> Makefile.config <<EOF
-ARCHDIRS=$arch $arch/lib $arch/abstractbb $arch/abstractbb/Impure
+ARCHDIRS=$arch $arch/lib $arch/abstractbb
 EXECUTE=kvx-cluster --syscall=libstd_scalls.so --
 CFLAGS= -D __KVX_COS__
 SIMU=kvx-cluster -- 
diff --git a/kvx/abstractbb/Impure/ImpConfig.v b/lib/Impure/ImpConfig.v
index dd9785b5..dd9785b5 100644
--- a/kvx/abstractbb/Impure/ImpConfig.v
+++ b/lib/Impure/ImpConfig.v
diff --git a/kvx/abstractbb/Impure/ImpCore.v b/lib/Impure/ImpCore.v
index 508b3f19..508b3f19 100644
--- a/kvx/abstractbb/Impure/ImpCore.v
+++ b/lib/Impure/ImpCore.v
diff --git a/kvx/abstractbb/Impure/ImpExtern.v b/lib/Impure/ImpExtern.v
index 8fb3cf3b..8fb3cf3b 100644
--- a/kvx/abstractbb/Impure/ImpExtern.v
+++ b/lib/Impure/ImpExtern.v
diff --git a/kvx/abstractbb/Impure/ImpHCons.v b/lib/Impure/ImpHCons.v
index 637116cc..637116cc 100644
--- a/kvx/abstractbb/Impure/ImpHCons.v
+++ b/lib/Impure/ImpHCons.v
diff --git a/kvx/abstractbb/Impure/ImpIO.v b/lib/Impure/ImpIO.v
index 6c02c395..6c02c395 100644
--- a/kvx/abstractbb/Impure/ImpIO.v
+++ b/lib/Impure/ImpIO.v
diff --git a/kvx/abstractbb/Impure/ImpLoops.v b/lib/Impure/ImpLoops.v
index 33376c19..33376c19 100644
--- a/kvx/abstractbb/Impure/ImpLoops.v
+++ b/lib/Impure/ImpLoops.v
diff --git a/kvx/abstractbb/Impure/ImpMonads.v b/lib/Impure/ImpMonads.v
index f01a2755..f01a2755 100644
--- a/kvx/abstractbb/Impure/ImpMonads.v
+++ b/lib/Impure/ImpMonads.v
diff --git a/kvx/abstractbb/Impure/ImpPrelude.v b/lib/Impure/ImpPrelude.v
index de4c7973..de4c7973 100644
--- a/kvx/abstractbb/Impure/ImpPrelude.v
+++ b/lib/Impure/ImpPrelude.v
diff --git a/kvx/abstractbb/Impure/LICENSE b/lib/Impure/LICENSE
index 65c5ca88..65c5ca88 100644
--- a/kvx/abstractbb/Impure/LICENSE
+++ b/lib/Impure/LICENSE
diff --git a/kvx/abstractbb/Impure/README.md b/lib/Impure/README.md
index 2b19d14a..2b19d14a 100644
--- a/kvx/abstractbb/Impure/README.md
+++ b/lib/Impure/README.md
diff --git a/kvx/abstractbb/Impure/ocaml/ImpHConsOracles.ml b/lib/Impure/ocaml/ImpHConsOracles.ml
index 2b66899b..2b66899b 100644
--- a/kvx/abstractbb/Impure/ocaml/ImpHConsOracles.ml
+++ b/lib/Impure/ocaml/ImpHConsOracles.ml
diff --git a/kvx/abstractbb/Impure/ocaml/ImpHConsOracles.mli b/lib/Impure/ocaml/ImpHConsOracles.mli
index 5075d176..5075d176 100644
--- a/kvx/abstractbb/Impure/ocaml/ImpHConsOracles.mli
+++ b/lib/Impure/ocaml/ImpHConsOracles.mli
diff --git a/kvx/abstractbb/Impure/ocaml/ImpIOOracles.ml b/lib/Impure/ocaml/ImpIOOracles.ml
index 9e63c12d..9e63c12d 100644
--- a/kvx/abstractbb/Impure/ocaml/ImpIOOracles.ml
+++ b/lib/Impure/ocaml/ImpIOOracles.ml
diff --git a/kvx/abstractbb/Impure/ocaml/ImpIOOracles.mli b/lib/Impure/ocaml/ImpIOOracles.mli
index 6064286a..6064286a 100644
--- a/kvx/abstractbb/Impure/ocaml/ImpIOOracles.mli
+++ b/lib/Impure/ocaml/ImpIOOracles.mli
diff --git a/kvx/abstractbb/Impure/ocaml/ImpLoopOracles.ml b/lib/Impure/ocaml/ImpLoopOracles.ml
index cb7625e5..cb7625e5 100644
--- a/kvx/abstractbb/Impure/ocaml/ImpLoopOracles.ml
+++ b/lib/Impure/ocaml/ImpLoopOracles.ml
diff --git a/kvx/abstractbb/Impure/ocaml/ImpLoopOracles.mli b/lib/Impure/ocaml/ImpLoopOracles.mli
index 194696a1..194696a1 100644
--- a/kvx/abstractbb/Impure/ocaml/ImpLoopOracles.mli
+++ b/lib/Impure/ocaml/ImpLoopOracles.mli