aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorGuillaume Melquiond <guillaume.melquiond@inria.fr>2020-09-08 18:29:00 +0200
committerXavier Leroy <xavier.leroy@college-de-france.fr>2022-04-25 16:38:45 +0200
commit9aacc59135071a979623ab177819cdbe9ce27056 (patch)
tree1d2069eba895833fdb3a7647c3cc37cea32a0de6 /Makefile
parentfb1f4545dfe861ff4d02816e295021a7e3061687 (diff)
downloadcompcert-9aacc59135071a979623ab177819cdbe9ce27056.tar.gz
compcert-9aacc59135071a979623ab177819cdbe9ce27056.zip
Upgrade to Flocq 4.0.
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile5
1 files changed, 2 insertions, 3 deletions
diff --git a/Makefile b/Makefile
index 2bc39c33..103a6cb3 100644
--- a/Makefile
+++ b/Makefile
@@ -84,13 +84,12 @@ GPATH=$(DIRS)
ifeq ($(LIBRARY_FLOCQ),local)
FLOCQ=\
- SpecFloatCompat.v \
Raux.v Zaux.v Defs.v Digits.v Float_prop.v FIX.v FLT.v FLX.v FTZ.v \
Generic_fmt.v Round_pred.v Round_NE.v Ulp.v Core.v \
- Bracket.v Div.v Operations.v Round.v Sqrt.v \
+ Bracket.v Div.v Operations.v Plus.v Round.v Sqrt.v \
Div_sqrt_error.v Mult_error.v Plus_error.v \
Relative.v Sterbenz.v Round_odd.v Double_rounding.v \
- Binary.v Bits.v
+ BinarySingleNaN.v Binary.v Bits.v
else
FLOCQ=
endif