diff options
| author | notin | 2007-11-28 18:07:28 +0000 |
|---|---|---|
| committer | notin | 2007-11-28 18:07:28 +0000 |
| commit | c6d34ae80622b409733776c3cc4ecf5fce6a8378 (patch) | |
| tree | 2e7626809950d881f9bd2446815d9acf358c7fff /doc/Makefile | |
| parent | 109e85dee481b9a00e6c27648ea62fc4048b0208 (diff) | |
Ajout de l'axiomatisation des entiers à la documentation de la librairie standard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10343 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/Makefile')
| -rw-r--r-- | doc/Makefile | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/doc/Makefile b/doc/Makefile index d9e9ab4201..f75d512631 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -82,6 +82,7 @@ clean: rm -f stdlib/index-list.html stdlib/index-body.html \ stdlib/Library.coqdoc.tex stdlib/library.files \ stdlib/library.files.ls + rm -f stdlib/html/*.html rm -f refman/euclid.ml{,i} refman/heapsort.ml{,i} rm -f common/version.tex rm -f refman/*.eps refman/Reference-Manual.html @@ -217,12 +218,12 @@ GLOBDUMP=$(COQSRC)/glob.dump LIBDIRS= Init Logic Bool Arith NArith ZArith QArith Relations Sets Setoids Lists Sorting Wellfounded IntMap FSets Reals Program # We avoid Strings as String.v contains unicode caracters that make latex fail -LIBDIRS+= Ints Ints/num -# LIBDIRS+= Ints/List Ints/Z -# LIBDIRS+= Numbers Numbers/Natural/Axioms Numbers/Natural/Binary Numbers/Natural/Peano Numbers/Integer/Axioms Numbers/Integer/NatPairs Numbers/Rational +LIBDIRS+= Ints Ints/num Ints/Z +LIBDIRS+= Numbers Numbers/NatInt Numbers/Natural/Abstract Numbers/Natural/Binary Numbers/Natural/Peano Numbers/Integer/Abstract Numbers/Integer/NatPairs Numbers/Integer/Binary -ALLTHEORIES_V=$(foreach dir, $(LIBDIRS), $(wildcard $(COQSRC)/theories/$(dir)/*.v)) +ALLTHEORIES_VO=$(foreach dir, $(LIBDIRS), $(wildcard $(COQSRC)/theories/$(dir)/*.vo)) +ALLTHEORIES_V=$(ALLTHEORIES_VO:%.vo=%.v) ALLTHEORIES_GLOB = $(ALLTHEORIES_V:%.v=%.glob) ### Standard library (browsable html format) |