From 7159e8142480fd0d851f3fd54b07dc8890f5b610 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@inria.fr>
Date: Tue, 7 Oct 2014 15:28:21 +0200
Subject: Upgrade to flocq 2.4.0

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

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 70b53a51..b6bf8e46 100644
--- a/Makefile
+++ b/Makefile
@@ -60,12 +60,12 @@ FLOCQ=\
   Fcalc_round.v Fcalc_sqrt.v                                                \
   Fprop_div_sqrt_error.v Fprop_mult_error.v Fprop_plus_error.v              \
   Fprop_relative.v Fprop_Sterbenz.v                                         \
-  Fappli_rnd_odd.v Fappli_IEEE.v Fappli_IEEE_bits.v
+  Fappli_rnd_odd.v Fappli_double_round.v Fappli_IEEE.v Fappli_IEEE_bits.v
 
 # General-purpose libraries (in lib/)
 
 LIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \
-  Iteration.v Integers.v Archi.v Fappli_IEEE_extra.v Floats.v \
+  Iteration.v Integers.v Archi.v Floats.v \
   Parmov.v UnionFind.v Wfsimpl.v \
   Postorder.v FSetAVLplus.v IntvSets.v
 
-- 
cgit