aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-05-21 16:38:45 +0000
committerGravatar aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-05-21 16:38:45 +0000
commited5578ecabad14a772c64f53265d168a51777045 (patch)
treeadea9da5a3e692ea51d898671173db6692e7cfed /Makefile
parent2c1c506d23118fb56fc07b4e334e0e1c7995e36b (diff)
Added Z and Q implementations with int31.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9846 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile3
1 files changed, 2 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 06e562f20..2de542be2 100644
--- a/Makefile
+++ b/Makefile
@@ -918,7 +918,8 @@ INTSVO=\
theories/Ints/num/GenDiv.vo theories/Ints/num/GenSqrt.vo \
theories/Ints/num/GenLift.vo theories/Ints/num/Zn2Z.vo\
theories/Ints/num/Nbasic.vo theories/Ints/num/NMake.vo \
- theories/Ints/BigN.vo
+ theories/Ints/BigN.vo theories/Ints/num/ZMake.vo \
+ theories/Ints/BigZ.vo theories/Ints/num/QMake.vo
# theories/Ints/List/ListAux.vo
# theories/Ints/List/LPermutation.vo theories/Ints/List/Iterator.vo \
# theories/Ints/List/ZProgression.vo