aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-ext.tex
AgeCommit message (Expand)Author
2018-03-15[Sphinx] Move chapter 2 to new infrastructureMaxime Dénès
2017-12-12Documenting the new options for printing "match".Hugo Herbelin
2017-10-24Fix part of 'Hard to find documentation for `(...) and `{...} #5631'Johannes Kloos
2017-09-22Avoid generated names for html pages of the reference manual (bug #4742).Guillaume Melquiond
2017-09-11Merge PR #1038: Fix Typo in Doc for `Set Parsing Explicit`Maxime Dénès
2017-09-08Fix Typo in Doc for `Set Parsing Explicit`staffehn
2017-08-31Document primitive projections in more detailMatthieu Sozeau
2017-07-14Update with non structurally recursivewilliam-lawvere
2017-07-07RefMan-ext: fix some typosWilliam Lawvere
2017-07-04Merge branch 'v8.6'Pierre-Marie Pédrot
2017-06-23Merge PR#740: Refactor documentation of records.Maxime Dénès
2017-06-16Refactor documentation of records.Théo Zimmermann
2017-06-14Prelude : no more autoload of plugins extraction and recdefPierre Letouzey
2017-06-13Document evar naming syntax.Théo Zimmermann
2017-04-12Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r...Maxime Dénès
2017-04-09Merge PR#460: Turning the printing primitive projection compatibility flag of...Maxime Dénès
2017-04-07Merge PR#485: Document Show MatchMaxime Dénès
2017-04-07Turning the printing primitive projection parameter flag off by default.Hugo Herbelin
2017-04-07Turning the printing primitive projection compatibility flag off by default.Hugo Herbelin
2017-03-23Documenting the grammar {| ... |} syntax for building records.Hugo Herbelin
2017-03-17Document Show Match, add ref to that in match variants/extensionsPaul Steckler
2017-03-14[toplevel] Remove unusable option -notopEmilio Jesus Gallego Arias
2016-11-08Update documentation of Arguments after recent changes.Maxime Dénès
2016-01-20Change $(...)$ to ltac:(...) in section 2.11. Fixes #4500.Maxime Dénès
2015-12-12Indexing and documenting some options.Pierre-Marie Pédrot
2015-12-10RefMan, ch. 4: Unify capitalization of "calculus of inductive constructions".Hugo Herbelin
2015-12-06RefMan, ch. 1 and 2: avoiding using the name "constant" whenHugo Herbelin
2015-12-02Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Hugo Herbelin
2015-11-26Adding the Printing Projections options to the index.Pierre-Marie Pédrot
2015-07-30Fix some broken Coq scripts in the documentation.Guillaume Melquiond
2015-07-22Remove obsolete documentation. (Fix bug #4238)Guillaume Melquiond
2015-04-01Fixing a few typos + some uniformization of writing in doc.Hugo Herbelin
2015-04-01More clarifications on loadpaths.Pierre-Marie Pédrot
2015-04-01Documenting "From * Require *" and clearing a bit the loadpath chapter.Pierre-Marie Pédrot
2015-02-17Separate index for vernacular options.Maxime Dénès
2015-02-12Fix typos about .vio files (thanks Arthur for spotting them)Enrico Tassi
2015-02-12Make clearer that "Remove Printing Let" does not influence destructuring let.Guillaume Melquiond
2015-02-10Prevent Latex from messing with backticks. (Fix for bug #3871)Guillaume Melquiond
2015-01-29Fix index of reference manual.Guillaume Melquiond
2015-01-29Remove some "Warning:" from the reference manual.Guillaume Melquiond
2015-01-24Reference Manual: Documenting new printing of evars and new effect ofHugo Herbelin
2015-01-15Move explanations about primitive projections to the manual.Matthieu Sozeau
2014-12-09refman: switch all source files to utf8Pierre Letouzey
2014-10-22Move 'Arguments: clear implicits' to 2.7.4 (Close 2891)Enrico Tassi
2014-09-29typoEnrico Tassi
2014-09-18seems to fix a looping coq-tex (when compiled with camlp4)Pierre Boutillier
2014-09-04Documenting the [Variant] type definition and the [Nonrecursive Elimination S...Arnaud Spiwack
2014-09-03sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.texPierre Boutillier
2014-09-03Update RefMan with respect to new loadpath managementPierre Boutillier
2014-08-25"allows to", like "allowing to", is improperJason Gross