aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorGuillaume Melquiond <guillaume.melquiond@inria.fr>2020-12-28 15:53:36 +0100
committerGitHub <noreply@github.com>2020-12-28 15:53:36 +0100
commitd4513f41c54869c9b4ba96ab79d50933a1d5c25a (patch)
treeb5ef5b74c19f386791d1f572c45b6b7af0e90451 /Makefile
parent548e62be073aa5a7b39d5826cd72681daef7c6a1 (diff)
downloadcompcert-kvx-d4513f41c54869c9b4ba96ab79d50933a1d5c25a.tar.gz
compcert-kvx-d4513f41c54869c9b4ba96ab79d50933a1d5c25a.zip
Update Flocq to 3.4.0 (#383)
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile1
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index 4b0b5761..73f8f172 100644
--- a/Makefile
+++ b/Makefile
@@ -57,6 +57,7 @@ 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 \