aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-syn.tex
AgeCommit message (Expand)Author
2018-03-15[Sphinx] Move chapter 12 to new infrastructureMaxime Dénès
2018-02-22Document Arguments extra scopes flagJasper Hugunin
2018-02-20Documenting use of primitive entry names for restricting syntax in notations.Hugo Herbelin
2018-02-20Extended documentation for notations referring to binders.Hugo Herbelin
2018-02-20A first step at refreshing and documenting the new feature.Hugo Herbelin
2017-09-22Avoid generated names for html pages of the reference manual (bug #4742).Guillaume Melquiond
2017-08-22Fix obsolete description of real numerals.Guillaume Melquiond
2017-07-05Merge PR #850: Improve grammar in RefMan-Gal and RefMan-synMaxime Dénès
2017-07-04Merge branch 'v8.6'Pierre-Marie Pédrot
2017-07-01Update RefMan-syn.texwilliam-lawvere
2017-07-01RefMan-syn: grammar editWilliam Lawvere
2017-06-23Fix Bug #5574, document function scopePaul Steckler
2017-06-13doc: improve grammar of RefMan-synWilliam Lawvere
2017-03-23Merge PR#433: doc: fix a French-ismMaxime Dénès
2017-03-14doc: fix a French-ismValentin Robert
2017-03-09Typo doc notations.Hugo Herbelin
2017-03-09Clarifying doc about interpretation of scopes in notations (#5386).Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 01:25:59 +0000