aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/common
Commit message (Expand)AuthorAge
* Documenting the grammar {| ... |} syntax for building records.Gravatar Hugo Herbelin2017-03-23
* Fix broken documentation in presence of \zeroone{... \tt ...}.Gravatar Guillaume Melquiond2016-12-06
* Update copyright on documentation cover.Gravatar Maxime Dénès2016-11-30
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-24
|\
| * FIX: HTML version of Chapter 4 of the Reference ManualGravatar Matej Kosik2016-04-12
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Updating and improving the documentation of intros patterns.Gravatar Hugo Herbelin2016-01-14
|/
* ENH: examples for 'strict positivity' were expandedGravatar Matej Kosik2015-12-10
* CLEANUP: s/List_A/List~A/gGravatar Matej Kosik2015-12-10
* CLEANUP: superfluous examples were removedGravatar Matej Kosik2015-12-10
* ENH: new example: "even"Gravatar Matej Kosik2015-12-10
* ALPHA-CONVERSION: s/Length/has_length/gGravatar Matej Kosik2015-12-10
* ENH: The beginning of Section 4.5 (Inductive declarations) was changed in ord...Gravatar Matej Kosik2015-12-10
* RefMan, ch. 4: Removing the local context of inductive definitions.Gravatar Hugo Herbelin2015-12-10
* RefMan, ch. 4: Adding discharging of inductive types.Gravatar Hugo Herbelin2015-12-10
* RefMan, ch. 4: In chapter 4 about CIC, renounced to keep a localGravatar Hugo Herbelin2015-12-10
* RefMan, ch. 4: Reformulating introduction of the chapter on CIC, beingGravatar Hugo Herbelin2015-12-10
* Remove some outdated files and fix permissions.Gravatar Guillaume Melquiond2015-07-31
* Separate index for vernacular options.Gravatar Maxime Dénès2015-02-17
* Refresh some copyright headers.Gravatar Maxime Dénès2015-01-13
* Added more informative messages about bullets.Gravatar Pierre Courtieu2015-01-05
* refman: switch all source files to utf8Gravatar Pierre Letouzey2014-12-09
* refman: remove ?uri=referer in urls pointing to validator.w3.orgGravatar Pierre Letouzey2014-12-09
* refman: xhtml validity of the cover pageGravatar Pierre Letouzey2014-12-09
* doc: improved xhtml compatibility (cover, header,...)Gravatar Pierre Letouzey2014-12-09
* doc/stdlib: fix the html charset in header.html and coGravatar Pierre Letouzey2014-12-09
* doc: version number in cover.html + updates in coq.inria.fr styleGravatar Pierre Letouzey2014-12-09
* Port to trunk commit r16062 of v8.4 (Correction des entêtes pour la document...Gravatar notin2014-12-09
* Port to trunk the old commit r14895 of v8.4 (styles for the stdlib documentat...Gravatar notin2014-12-09
* doc: version number in cover.html + updates in coq.inria.fr styleGravatar Pierre Letouzey2014-11-07
* Making references to Proof General and CoqIDE uniform in Reference Manual.Gravatar Hugo Herbelin2014-08-05
* Beautify tactic documentation a bit more.Gravatar gmelquio2012-09-16
* Remove superfluous spaces and commas in tactic documentation.Gravatar gmelquio2012-09-16
* Improving rendering of ldots in doc (partially done, there are tooGravatar herbelin2012-08-11
* Added support for option Local (at module level) in Tactic Notation.Gravatar herbelin2012-08-11
* Improving rendering of ...-separated lists and sequences in referenceGravatar herbelin2012-08-11
* Documenting eta-conversion.Gravatar herbelin2012-08-08
* More standard layout for \lambda in chapter CIC.Gravatar herbelin2012-08-08
* Documentation of records defined with the keywords Inductive andGravatar aspiwack2012-04-13
* Version number, copyright, credits: missing updates.Gravatar herbelin2011-12-25
* Html page titlesGravatar pboutill2011-12-07
* Ajout d'une feuille de style pour les définitions spécifiques à Hevea + di...Gravatar notin2010-06-23
* Mise à jour des liens au site Coq (suite à la MAJ de la redirection DNS de ...Gravatar notin2010-06-23
* Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".Gravatar herbelin2010-06-08
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Modification du style du manuel de référenceGravatar notin2009-02-11
* Backporting from v8.2 to trunk:Gravatar herbelin2009-01-18
* Updated datesGravatar herbelin2009-01-13
* - Fixed bug #2021 (uncaught exception with injection/discriminate whenGravatar herbelin2009-01-01