aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-syn.tex
AgeCommit message (Expand)Author
2016-12-16Fix incorrect documentation that prevents successful compilation (bug #5265).Guillaume Melquiond
2016-11-08Update documentation of Arguments after recent changes.Maxime Dénès
2016-07-17More examples of recursive notations, with emphasis in reference manual.Hugo Herbelin
2016-06-28Documenting the "only printing" notation flag.Pierre-Marie Pédrot
2016-05-15Fix a really small doc typoRicky Elrod
2015-08-14Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080Jason Gross
2015-06-26Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Lionel Rieg
2015-03-13Fixing #4127 (command for locating exists notation in refman changed).Hugo Herbelin
2015-03-05Preprend Fail to all the expected failures in the documentation.Guillaume Melquiond
2015-02-17Separate index for vernacular options.Maxime Dénès
2015-02-05Fix some documentation typos.Guillaume Melquiond
2015-01-29Fix index of reference manual.Guillaume Melquiond
2014-08-05Doc: uconstr now has a tactic notation entry.Arnaud Spiwack
2012-08-11Added support for option Local (at module level) in Tactic Notation.herbelin
2012-04-13Uniformisation in the documentation: remove the use of 'coinductive' inaspiwack
2012-03-26Slight change in the semantics of arguments scopes: scopes can noherbelin
2011-12-06Documentation for Arguments + notation scopesgareuselesinge
2011-09-02Bug 2589: Documentation patch of Hendrik Tewspboutill
2011-04-28Adding "Tactic Notation" in doc index.herbelin
2010-07-22Extension of the recursive notations mechanismherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-11-11Added support for multiple where-clauses in Inductive and co (see wish #2163).herbelin
2009-11-02Correction du bug #2175notin
2009-10-26New cleaning phase of the Local/Global option managementherbelin
2009-10-25Improved the treatment of Local/Global options (noneffective Local onherbelin
2009-01-19- Structuring Numbers and fixing Setoid in stdlib's doc.herbelin
2009-01-13- Standardized prefix use of "Local"/"Global" modifiers as decided inherbelin
2008-10-11Backporting 11445 from 8.2 to trunk (negative conditions inherbelin
2008-07-01Documentation Prop<=Set et Arguments Scope Globalherbelin
2008-06-08- Extension de "generalize" en "generalize c as id at occs".herbelin
2008-05-12MAJ et bricoles diversesherbelin
2008-05-05Minor updates in the documentation of notations.glondu
2008-03-30Ajout d'abbréviations/notations paramétriquesherbelin
2008-01-05Standardisation du format des références croisées vers Figure, Section, Ch...herbelin
2007-04-17Changed many refman/*.tex files. Put \label and \index commands that immediat...emakarov
2006-07-05Mise à jour scopes prédéfinis et Tactic Notation pour tacticalsherbelin
2006-07-04Doc Print Grammar patternherbelin
2006-02-24Modification des propriétés des fichiers .tex (svn:executable)notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty
2006-02-23Nettoyage de l'archive doc et restructuration avant intégration à l'archiveherbelin