aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile3
1 files changed, 2 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 81bac199a7..a1db4ccebd 100644
--- a/Makefile
+++ b/Makefile
@@ -367,7 +367,8 @@ BOOLVO=theories/Bool/Bool.vo theories/Bool/IfProp.vo \
ZARITHVO=theories/ZArith/Wf_Z.vo theories/ZArith/Zsyntax.vo \
theories/ZArith/ZArith.vo theories/ZArith/auxiliary.vo \
theories/ZArith/ZArith_dec.vo theories/ZArith/fast_integer.vo \
- theories/ZArith/Zmisc.vo theories/ZArith/zarith_aux.vo
+ theories/ZArith/Zmisc.vo theories/ZArith/zarith_aux.vo \
+ theories/ZArith/Zhints.vo
LISTSVO=theories/Lists/List.vo theories/Lists/PolyListSyntax.vo \
theories/Lists/ListSet.vo theories/Lists/Streams.vo \