aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/common/macros.tex
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
* 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
* | 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
* Added more informative messages about bullets.Gravatar Pierre Courtieu2015-01-05
* 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
* Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".Gravatar herbelin2010-06-08
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Backporting from v8.2 to trunk:Gravatar herbelin2009-01-18
* - Fixed bug #2021 (uncaught exception with injection/discriminate whenGravatar herbelin2009-01-01
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* Backporting 11445 from 8.2 to trunk (negative conditions inGravatar herbelin2008-10-11
* A pass on documentation: Gravatar msozeau2008-09-14
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* Nouvelle doc pour les modules.Gravatar soubiran2008-05-23
* Correction bug 1838 + doc modules.Gravatar soubiran2008-04-21
* - Un peu de doc, préparation du CHANGES pour la release.Gravatar herbelin2008-04-15
* - Documentation des nouvelles options d'implicites (Set Strongly StrictGravatar herbelin2008-02-06
* Some changes to eliminate Hevea warnings.Gravatar emakarov2007-04-10
* Relecture/nettoyage chapitre Gallina; déplacement section FunctionGravatar herbelin2007-02-07
* Documentation de lazymatch et des extensions de idtac et failGravatar herbelin2006-07-11
* Ajout taclevelGravatar herbelin2006-07-05
* Documentation or-patternGravatar herbelin2006-07-04
* Nettoyage de l'archive doc et restructuration avant intégration à l'archiveGravatar herbelin2006-02-23