aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 1367b87812..e34dd8a54b 100644
--- a/Makefile
+++ b/Makefile
@@ -384,7 +384,7 @@ ARITHVO=theories/Arith/Arith.vo theories/Arith/Gt.vo \
theories/Arith/Mult.vo theories/Arith/Even.vo \
theories/Arith/EqNat.vo theories/Arith/Peano_dec.vo \
theories/Arith/Euclid.vo theories/Arith/Plus.vo \
- theories/Arith/Wf_nat.vo \
+ theories/Arith/Wf_nat.vo theories/Arith/Max.vo \
# theories/Arith/Div.vo
BOOLVO=theories/Bool/Bool.vo theories/Bool/IfProp.vo \