aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...Gravatar letouzey2009-03-20
* RefMan: a label defined twiceGravatar letouzey2009-03-14
* Coqdep: remove references to obsolete .zi and Require Implementation stuffGravatar letouzey2009-03-14
* doc et CHANGES pour la commande TimeoutGravatar barras2009-03-04
* maj de la faq: correction de l'exemple field qui compilait plus en 8.2, corre...Gravatar jnarboux2009-02-17
* Modification du style du manuel de référenceGravatar notin2009-02-11
* Solves some warning and hides some not-bad ones in doc. It remains aGravatar herbelin2009-01-29
* - Fixed various Overfull in documentation.Gravatar herbelin2009-01-27
* Fixes in the documentation of [dependent induction] and test-suiteGravatar msozeau2009-01-22
* Fixed bug 2030 (bad syntax for "test" in doc compilation) [see 11824Gravatar herbelin2009-01-21
* Added some missing statements for proof folding and correctedGravatar vgross2009-01-20
* Added proof folding into CoqIde. See RefMan for using it.Gravatar vgross2009-01-20
* Propriétés svn pour les filtres latexGravatar notin2009-01-19
* - Structuring Numbers and fixing Setoid in stdlib's doc.Gravatar herbelin2009-01-19
* Backporting from v8.2 to trunk:Gravatar herbelin2009-01-18
* Last changes in type class syntax: Gravatar msozeau2009-01-18
* Updated datesGravatar herbelin2009-01-13
* - Standardized prefix use of "Local"/"Global" modifiers as decided inGravatar herbelin2009-01-13
* Minor doc fixes:Gravatar msozeau2009-01-08
* Fixed two problems:Gravatar herbelin2009-01-03
* - Fixed bug #2021 (uncaught exception with injection/discriminate whenGravatar herbelin2009-01-01
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* Produce better html code with coqdoc and improve doc:Gravatar msozeau2008-12-29
* - coq_makefile: target install now respects the original tree structureGravatar herbelin2008-12-24
* Nettoyage des variables Coq et amélioration de coqmktop. LesGravatar notin2008-12-19
* Extraction Blacklist : a new command for avoiding conflicts with existing filesGravatar letouzey2008-12-16
* Fixes in the type classes documentation:Gravatar msozeau2008-12-14
* About "apply in":Gravatar herbelin2008-12-09
* Inductive parameters: nicer doc examples and error messageGravatar letouzey2008-11-28
* - Fixed minor bug #1994 in the tactic chapter of the manual [doc]Gravatar herbelin2008-11-22
* Fix typo in omega docGravatar glondu2008-11-19
* Document native "Declare ML Module"Gravatar glondu2008-10-29
* - Fixed many "Theorem with" bugs.Gravatar herbelin2008-10-27
* Fix doc of apply in (see coq-club message 26 September 2008)Gravatar herbelin2008-10-24
* Various coqdoc improvements:Gravatar msozeau2008-10-22
* Renommage "Global Instance" en "Instance Global" pour uniformisationGravatar herbelin2008-10-20
* - Export de pattern_ident vers les ARGUMENT EXTEND and co.Gravatar herbelin2008-10-19
* report de la révision r11451 (nouveau style html pour le manuel de référence)Gravatar notin2008-10-14
* Backporting 11445 from 8.2 to trunk (negative conditions inGravatar herbelin2008-10-11
* Update stdlib html templateGravatar glondu2008-09-15
* A pass on documentation: Gravatar msozeau2008-09-14
* Add user syntax for creating hint databases [Create HintDb fooGravatar msozeau2008-09-14
* Mise à jour des fichiers README et INSTALL de la doc (bug #1921) + suppressi...Gravatar notin2008-08-06
* correction : coqart is already publishedGravatar jnarboux2008-08-06
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Typo in docGravatar glondu2008-07-29
* Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized theGravatar herbelin2008-07-23
* - Rebranchement backtrack du langage déclaratif dans CoqideGravatar herbelin2008-07-18
* - Suppression de Rstar/Newman peu utilisables comme biblio (encodageGravatar herbelin2008-07-17
* update doc MicromegaGravatar fbesson2008-07-13