aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/RefMan-ext.tex
Commit message (Expand)AuthorAge
...
* Documenting the tactic-in-term construction.Gravatar Pierre-Marie Pédrot2013-12-11
* Silence some warning about references in documentation.Gravatar Guillaume Melquiond2013-12-03
* First stab at documenting Canonical StructuresGravatar Enrico Tassi2013-11-29
* Manual fixed w.r.t. STMGravatar gareuselesinge2013-08-08
* Documentation of the "Local Definition" command.Gravatar ppedrot2013-03-11
* Added missing documentation of Set Printing Existential Instances.Gravatar herbelin2013-02-21
* Improving rendering of ...-separated lists and sequences in referenceGravatar herbelin2012-08-11
* Documentation of records defined with the keywords Inductive andGravatar aspiwack2012-04-13
* Added documentation for "Set Parsing Explicit" + fixed mistakenlyGravatar herbelin2012-01-20
* Fixed a Not_found bug when declaring in a section some implicitGravatar herbelin2011-12-18
* Command Arguments: standardizing format of error messages and American spelling.Gravatar herbelin2011-12-17
* Documentation of Arguments + implicitsGravatar gareuselesinge2011-12-06
* This adds two option tables 'Printing Record' and 'Printing Constructor'Gravatar herbelin2011-07-16
* This option disables the use of the '{| field := ... |}' notationGravatar herbelin2011-07-16
* @ in index of refman (last request of bug 2494)Gravatar pboutill2011-04-08
* Fixing bug #2475 (ability to use binders in the syntax of fields was not in doc)Gravatar herbelin2011-04-06
* Fix formatting issue in refmanGravatar glondu2011-01-12
* Add "Print Sorted Universes"Gravatar glondu2011-01-11
* Document DOT output of universe graphGravatar glondu2010-11-02
* Added multiple implicit arguments rules per name.Gravatar herbelin2010-10-03
* Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".Gravatar herbelin2010-06-08
* Correction in Function documentationGravatar jforest2010-05-06
* Applying François Garillot's patch (#2261 in bug tracker) for extendedGravatar herbelin2010-04-22
* Document Generalizable Variables, and change syntax to Gravatar msozeau2009-11-15
* Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.Gravatar gmelquio2009-11-04
* Fixed some typos in the reference manual.Gravatar gmelquio2009-10-29
* - Fixed various Overfull in documentation.Gravatar herbelin2009-01-27
* Last changes in type class syntax: Gravatar msozeau2009-01-18
* - Standardized prefix use of "Local"/"Global" modifiers as decided inGravatar herbelin2009-01-13
* Lissage de la gestion des chemins de chargement de fichiers :Gravatar herbelin2008-06-29
* Modif un peu gadget (??): on peut écrire "set (f n:=t)" pour Gravatar herbelin2008-04-26
* - Un peu de doc, préparation du CHANGES pour la release.Gravatar herbelin2008-04-15
* Fix examples in Program documentation and add comindexes for the variousGravatar msozeau2008-03-23
* Fix the clrewrite tactic, change Relations.v to work on relations in PropGravatar msozeau2008-02-09
* Documentation of CHANGES and refman doc for the implicit argument binderGravatar msozeau2008-02-08
* - Documentation des nouvelles options d'implicites (Set Strongly StrictGravatar herbelin2008-02-06
* Unification de TacLetRecIn et TacLetIn. En particulier, on peutGravatar herbelin2008-02-01
* Finish let| implementation and document itGravatar msozeau2008-01-31
* Standardisation du format des références croisées vers Figure, Section, Ch...Gravatar herbelin2008-01-05
* Ajout possibilité d'options à trois mots.Gravatar herbelin2007-04-29
* Fixed some typos.Gravatar glondu2007-04-18
* Changed many refman/*.tex files. Put \label and \index commands that immediat...Gravatar emakarov2007-04-17
* Cleaned doc/common/title.tex file. Increased the space under headersGravatar emakarov2007-04-12
* Meilleur anglais (cf 9619)Gravatar herbelin2007-02-07
* Relecture/nettoyage chapitre Gallina; déplacement section FunctionGravatar herbelin2007-02-07
* Documentation de "Set Printing Universes", "Print Universes" (anciennementGravatar herbelin2006-10-28
* Documentation Declare Implicit Tactic, Print Canonical Projections, ... + lé...Gravatar herbelin2006-07-07
* Documentation or-patternGravatar herbelin2006-07-04
* Nettoyage de l'archive doc et restructuration avant intégration à l'archiveGravatar herbelin2006-02-23