aboutsummaryrefslogtreecommitdiff
path: root/doc/stdlib/index-list.html.template
AgeCommit message (Collapse)Author
2012-06-12make sure that documentation compilation works after adding files forbertot
arc tangent and computations of PI approximations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15436 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-13MSetRBT : implementation of MSets via Red-Black treesletouzey
Initial contribution by Andrew Appel, many ulterior modifications by myself. Interest: red-black trees maintain logarithmic depths as AVL, but they do not rely on integer height annotations as AVL, allowing interesting performance when computing in Coq or after standard extraction. More on this topic in the article by A. Appel. The common parts of MSetAVL and MSetRBT are shared in a new file MSetGenTree which include the definition of tree and functions such as mem fold elements compare subset. Note that the height of AVL trees is now the first arg of the Node constructor instead of the last one. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15168 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-01Improved synchronisation of stdlib index page with current library state.herbelin
- Made generation of index page fail if a file is missing in list or listed but unbound in existing theories - Added a file hidden-files to optionally list library files not to show in the index page (though it is currently empty) - Added directory Unicode (why not to have it after all?) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14957 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-31index-list.html.template: add missing filespboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14955 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-04doc/stdlib: Update the list of ZArith filesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14255 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-06update of the file list in doc/stdlibletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14112 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-05Restore documentation of library String which was removed in 2007 (r10049)herbelin
probably inadvertantly since it is not reported in the commit log. (Thanks to Cédric who noticed it.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13877 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-10Remove obsolete TheoryListglondu
This library is no longer used anywhere, and its contents is very... let's say historical... More seriously, many (and presumably the most useful) stuff that used to be there are in List, now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13828 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-06Numbers and bitwise functions.letouzey
See NatInt/NZBits.v for the common axiomatization of bitwise functions over naturals / integers. Some specs aren't pretty, but easier to prove, see alternate statements in property functors {N,Z}Bits. Negative numbers are considered via the two's complement convention. We provide implementations for N (in Ndigits.v), for nat (quite dummy, just for completeness), for Z (new file Zdigits_def), for BigN (for the moment partly by converting to N, to be improved soon) and for BigZ. NOTA: For BigN.shiftl and BigN.shiftr, the two arguments are now in the reversed order (for consistency with the rest of the world): for instance BigN.shiftl 1 10 is 2^10. NOTA2: Zeven.Zdiv2 is _not_ doing (Zdiv _ 2), but rather (Zquot _ 2) on negative numbers. For the moment I've kept it intact, and have just added a Zdiv2' which is truly equivalent to (Zdiv _ 2). To reorganize someday ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13689 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-10Integer division: quot and rem (trunc convention) in addition to div and modletouzey
(floor convention). We follow Haskell naming convention: quot and rem are for Round-Toward-Zero (a.k.a Trunc, what Ocaml, C, Asm do by default, cf. the ex-ZOdiv file), while div and mod are for Round-Toward-Bottom (a.k.a Floor, what Coq does historically in Zdiv). We use unicode ÷ for quot, and infix rem for rem (which is actually remainder in full). This way, both conventions can be used at the same time. Definitions (and proofs of specifications) for div mod quot rem are migrated in a new file Zdiv_def. Ex-ZOdiv file is now Zquot. With this new organisation, no need for functor application in Zdiv and Zquot. On the abstract side, ZAxiomsSig now provides div mod quot rem. Zproperties now contains properties of them. In NZDiv, we stop splitting specifications in Common vs. Specific parts. Instead, the NZ specification is be extended later, even if this leads to a useless mod_bound_pos, subsumed by more precise axioms. A few results in ZDivTrunc and ZDivFloor are improved (sgn stuff). A few proofs in Nnat, Znat, Zabs are reworked (no more dependency to Zmin, Zmax). A lcm (least common multiple) is derived abstractly from gcd and division (and hence available for nat N BigN Z BigZ :-). In these new files NLcm and ZLcm, we also provide some combined properties of div mod quot rem gcd. We also provide a new file Zeuclid implementing a third division convention, where the remainder is always positive. This file instanciate the abstract one ZDivEucl. Operation names are ZEuclid.div and ZEuclid.modulo. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13633 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-05Numbers: axiomatization, properties and implementations of gcdletouzey
- For nat, we create a brand-new gcd function, structural in the sense of Coq, even if it's Euclid algorithm. Cool... - We re-organize the Zgcd that was in Znumtheory, create out of it files Pgcd, Ngcd_def, Zgcd_def. Proofs of correctness are revised in order to be much simpler (no omega, no advanced lemmas of Znumtheory, etc). - Abstract Properties NZGcd / ZGcd / NGcd could still be completed, for the moment they contain up to Gauss thm. We could add stuff about (relative) primality, relationship between gcd and div,mod, or stuff about parity, etc etc. - Znumtheory remains as it was, apart for Zgcd and correctness proofs gone elsewhere. We could later take advantage of ZGcd in it. Someday, we'll have to switch from the current Zdivide inductive, to Zdivide' via exists. To be continued... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13623 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-02Numbers : log2. Abstraction, properties and implementations.letouzey
Btw, we finally declare the original Zpower as the power on Z. We should switch to a more efficient one someday, but in the meantime BigN is proved with respect to the old one. TODO: reform Zlogarithm with respect to Zlog_def git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13606 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-02Move stuff about positive into a distinct PArith subdirletouzey
Beware! after this, a ./configure must be done. It might also be a good idea to chase any phantom .vo remaining after a make clean git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13601 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-16FSetPositive: sets of positive inspired by FMapPositive.letouzey
Contributed by Alexandre Ren, Damien Pous, and Thomas Braibant. I've also included a MSets version, hence FSetPositive might become soon a mere wrapper for MSetPositive, as for other FSets implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13287 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-28Update of documentation for the standard library (cf. #2332)letouzey
This is a slightly modified version of the patch proposed in #2332 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13209 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Remove useless MonoList.vglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12339 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-19- Structuring Numbers and fixing Setoid in stdlib's doc.herbelin
- Adding ability to use "_" in syntax for binders (as in "exists _:nat, True"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11804 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-18Backporting from v8.2 to trunk:herbelin
- Filtering of doc compilation messages (11793,11795,11796). - Fixing bug #1925 and cleaning around bug #1894 (11796, 11801). - Adding some tests. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11802 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-29Produce better html code with coqdoc and improve doc:msozeau
- correct nesting of a and div (fixes bug #2022) - use span instead of div for inline parts - fix standard lib template missing/new links - use -g to produce the stdlib doc (no proofs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11724 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-09-15Update stdlib html templateglondu
Hints from compilation warnings git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11411 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-07Fix library index template and associated script.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11067 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-03Fix setoid_rewrite documentation examples.msozeau
Debug handling of identifiers in coqdoc (should work with modules and sections) and add missing macros. Move theories/Program to THEORIESVO to put the files in the standard library documentation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11046 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-19some references to IntMap forgotten in last commitletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10700 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08updates concerning FSetsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10527 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-28Ajout de l'axiomatisation des entiers à la documentation de la librairie ↵notin
standard git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10343 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-08A better Program documentation. Include it in the generated stdlib doc.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10061 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-25Modifications de la construction de la documentation de la librairienotin
standard: - ajout d'une entrée dans le Makefile principal pour le fichier de globalisations glob.dump - modifications de doc/Makefile et de l'index html pour gérer les nouveaux fichiers de la librairie standard (en part. ceux dans Ints) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10049 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-16Correction du bug #1441notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9712 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-11Typo + ajout Qcanon.vherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9366 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09MAJ liste fichiers doc stdlibherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8937 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-26Support des modules dans Coqdocnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8863 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-28- correction d'un bug dans coqdoc (multi_index)notin
- modif. de la génération de la doc de stdlib git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8669 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-25 r8709@thot: notin | 2006-03-25 01:48:46 +0100notin
- Ajout de FSets dans la doc de stdlib - coqdoc copie la feuille de style dans le répertoire courant git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8663 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-23Mise à jour des Makefile, ajout licences, corrections mineures suite àherbelin
restructuration du répertoire de documentation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8607 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 23:58:36 +0000