Use Flocq for floats

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 14 insertions, 2 deletions

diff --git a/Makefile b/Makefile
index 793a4d4..175f773 100644
--- a/Makefile
+++ b/Makefile
@@ -12,7 +12,8 @@
 
 include Makefile.config
 
-DIRS=lib common $(ARCH)/$(VARIANT) $(ARCH) backend cfrontend driver
+DIRS=lib common $(ARCH)/$(VARIANT) $(ARCH) backend cfrontend driver \
+  flocq/Core flocq/Prop flocq/Calc flocq/Appli
 
 INCLUDES=$(patsubst %,-I %, $(DIRS))
 
@@ -36,6 +37,17 @@ OCB_OPTIONS_CHECKLINK=\
 VPATH=$(DIRS)
 GPATH=$(DIRS)
 
+# Flocq
+FLOCQ_CORE=Fcore_float_prop.v Fcore_Zaux.v Fcore_rnd_ne.v Fcore_FTZ.v \
+  Fcore_FLT.v Fcore_defs.v Fcore_Raux.v Fcore_ulp.v Fcore_rnd.v Fcore_FLX.v \
+  Fcore_FIX.v Fcore_digits.v Fcore_generic_fmt.v Fcore.v
+FLOCQ_PROP=Fprop_Sterbenz.v Fprop_mult_error.v Fprop_relative.v \
+  Fprop_div_sqrt_error.v Fprop_plus_error.v
+FLOCQ_CALC=Fcalc_ops.v Fcalc_bracket.v Fcalc_sqrt.v Fcalc_div.v Fcalc_round.v \
+  Fcalc_digits.v
+FLOCQ_APPLI=Fappli_IEEE_bits.v Fappli_IEEE.v
+FLOCQ=$(FLOCQ_CORE) $(FLOCQ_PROP) $(FLOCQ_CALC) $(FLOCQ_APPLI)
+
 # General-purpose libraries (in lib/)
 
 LIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \
@@ -90,7 +102,7 @@ DRIVER=Compiler.v Complements.v
 
 # All source files
 
-FILES=$(LIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER)
+FILES=$(LIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) $(FLOCQ)
 
 # Symbolic links vs. copy