From 9aacc59135071a979623ab177819cdbe9ce27056 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Tue, 8 Sep 2020 18:29:00 +0200
Subject: Upgrade to Flocq 4.0.

---
 Makefile | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'Makefile')

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
-- 
cgit