aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorherbelin2003-11-21 21:30:11 +0000
committerherbelin2003-11-21 21:30:11 +0000
commit06eaa6883b276c3e14509ced57ef1e63f2ec21e4 (patch)
tree46ae3bccdd9cc3e07063f75f97ddd3f45afa16c2 /Makefile
parente5644fac0cce2040961a451eeeda14a88cf5405b (diff)
Extraction des lemmes sur convert/nat_of_P de BinPos vers Pnat; ajout Pcase et Pcompare_antisym
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4962 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index aa5ac43e85..9e0cc51fd7 100644
--- a/Makefile
+++ b/Makefile
@@ -582,8 +582,8 @@ BOOLVO=\
theories/Bool/Bvector.vo
NARITHVO=\
- theories/NArith/BinPos.vo theories/NArith/BinNat.vo \
- theories/NArith/NArith.vo
+ theories/NArith/BinPos.vo theories/NArith/Pnat.vo \
+ theories/NArith/BinNat.vo theories/NArith/NArith.vo
ZARITHVO=\
theories/ZArith/BinInt.vo \