aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile4
1 files changed, 2 insertions, 2 deletions
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