From 028fffbb055b2966b6205c5eaa432d6c4e22f677 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 5 Mar 2020 17:14:14 +0100
Subject: more about extraction and linking

---
 Makefile | 1 +
 1 file changed, 1 insertion(+)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 2cd40800..4fc94a58 100644
--- a/Makefile
+++ b/Makefile
@@ -57,6 +57,7 @@ FLOCQ=\
 # General-purpose libraries (in lib/)
 
 VLIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \
+  HashedSet.v \
   Iteration.v Zbits.v Integers.v Archi.v IEEE754_extra.v Floats.v \
   Parmov.v UnionFind.v Wfsimpl.v \
   Postorder.v FSetAVLplus.v IntvSets.v Decidableplus.v BoolEqual.v
-- 
cgit