aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorletouzey2001-11-21 14:34:18 +0000
committerletouzey2001-11-21 14:34:18 +0000
commiteee1234e45b50f89cb7ebe71b1ac5e837c724909 (patch)
tree56d2c625b9e99f836ff6115af0f8534c870a1699 /Makefile
parent64401334b9707f74b9e9fedfed64f10c5e7a01b9 (diff)
remise au gout du jour du repertoire theories/Sorting de la V6.3
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2231 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile7
1 files changed, 6 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index e34dd8a54b..52be6f90b5 100644
--- a/Makefile
+++ b/Makefile
@@ -387,6 +387,10 @@ ARITHVO=theories/Arith/Arith.vo theories/Arith/Gt.vo \
theories/Arith/Wf_nat.vo theories/Arith/Max.vo \
# theories/Arith/Div.vo
+SORTINGVO=theories/Sorting/Heap.vo \
+ theories/Sorting/Permutation.vo \
+ theories/Sorting/Sorting.vo
+
BOOLVO=theories/Bool/Bool.vo theories/Bool/IfProp.vo \
theories/Bool/Zerob.vo theories/Bool/DecBool.vo \
theories/Bool/Sumbool.vo theories/Bool/BoolEq.vo
@@ -454,7 +458,7 @@ SETOIDSVO=theories/Setoids/Setoid.vo
THEORIESVO = $(LOGICVO) $(ARITHVO) $(BOOLVO) $(ZARITHVO) $(LISTSVO) \
$(SETSVO) $(INTMAPVO) $(RELATIONSVO) $(WELLFOUNDEDVO) \
- $(REALSVO) $(SETOIDSVO)
+ $(REALSVO) $(SETOIDSVO) $(SORTINGVO)
$(THEORIESVO): states/initial.coq
@@ -470,6 +474,7 @@ intmap: $(INTMAPVO)
relations: $(RELATIONSVO)
wellfounded: $(WELLFOUNDEDVO)
reals: $(REALSVO)
+sorting: $(SORTING)
clean::
rm -f theories/*/*.vo