aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/RefMan-ext.tex
Commit message (Expand)AuthorAge
* [Sphinx] Move chapter 2 to new infrastructureGravatar Maxime Dénès2018-03-15
* Documenting the new options for printing "match".Gravatar Hugo Herbelin2017-12-12
* Fix part of 'Hard to find documentation for `(...) and `{...} #5631'Gravatar Johannes Kloos2017-10-24
* Avoid generated names for html pages of the reference manual (bug #4742).Gravatar Guillaume Melquiond2017-09-22
* Merge PR #1038: Fix Typo in Doc for `Set Parsing Explicit`Gravatar Maxime Dénès2017-09-11
|\
| * Fix Typo in Doc for `Set Parsing Explicit`Gravatar staffehn2017-09-08
* | Document primitive projections in more detailGravatar Matthieu Sozeau2017-08-31
|/
* Update with non structurally recursiveGravatar william-lawvere2017-07-14
* RefMan-ext: fix some typosGravatar William Lawvere2017-07-07
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\
| * Merge PR#740: Refactor documentation of records.Gravatar Maxime Dénès2017-06-23
| |\
| | * Refactor documentation of records.Gravatar Théo Zimmermann2017-06-16
* | | Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
| * | Document evar naming syntax.Gravatar Théo Zimmermann2017-06-13
| |/
* | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r...Gravatar Maxime Dénès2017-04-12
|\ \
* \ \ Merge PR#460: Turning the printing primitive projection compatibility flag of...Gravatar Maxime Dénès2017-04-09
|\ \ \
* \ \ \ Merge PR#485: Document Show MatchGravatar Maxime Dénès2017-04-07
|\ \ \ \
| | * | | Turning the printing primitive projection parameter flag off by default.Gravatar Hugo Herbelin2017-04-07
| | * | | Turning the printing primitive projection compatibility flag off by default.Gravatar Hugo Herbelin2017-04-07
| |/ / / |/| | |
| | * | Documenting the grammar {| ... |} syntax for building records.Gravatar Hugo Herbelin2017-03-23
| |/ / |/| |
| * | Document Show Match, add ref to that in match variants/extensionsGravatar Paul Steckler2017-03-17
| |/
* / [toplevel] Remove unusable option -notopGravatar Emilio Jesus Gallego Arias2017-03-14
|/
* Update documentation of Arguments after recent changes.Gravatar Maxime Dénès2016-11-08
* Change $(...)$ to ltac:(...) in section 2.11. Fixes #4500.Gravatar Maxime Dénès2016-01-20
* Indexing and documenting some options.Gravatar Pierre-Marie Pédrot2015-12-12
* RefMan, ch. 4: Unify capitalization of "calculus of inductive constructions".Gravatar Hugo Herbelin2015-12-10
* RefMan, ch. 1 and 2: avoiding using the name "constant" whenGravatar Hugo Herbelin2015-12-06
* Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Gravatar Hugo Herbelin2015-12-02
* Adding the Printing Projections options to the index.Gravatar Pierre-Marie Pédrot2015-11-26
* Fix some broken Coq scripts in the documentation.Gravatar Guillaume Melquiond2015-07-30
* Remove obsolete documentation. (Fix bug #4238)Gravatar Guillaume Melquiond2015-07-22
* Fixing a few typos + some uniformization of writing in doc.Gravatar Hugo Herbelin2015-04-01
* More clarifications on loadpaths.Gravatar Pierre-Marie Pédrot2015-04-01
* Documenting "From * Require *" and clearing a bit the loadpath chapter.Gravatar Pierre-Marie Pédrot2015-04-01
* Separate index for vernacular options.Gravatar Maxime Dénès2015-02-17
* Fix typos about .vio files (thanks Arthur for spotting them)Gravatar Enrico Tassi2015-02-12
* Make clearer that "Remove Printing Let" does not influence destructuring let.Gravatar Guillaume Melquiond2015-02-12
* Prevent Latex from messing with backticks. (Fix for bug #3871)Gravatar Guillaume Melquiond2015-02-10
* Fix index of reference manual.Gravatar Guillaume Melquiond2015-01-29
* Remove some "Warning:" from the reference manual.Gravatar Guillaume Melquiond2015-01-29
* Reference Manual: Documenting new printing of evars and new effect ofGravatar Hugo Herbelin2015-01-24
* Move explanations about primitive projections to the manual.Gravatar Matthieu Sozeau2015-01-15
* refman: switch all source files to utf8Gravatar Pierre Letouzey2014-12-09
* Move 'Arguments: clear implicits' to 2.7.4 (Close 2891)Gravatar Enrico Tassi2014-10-22
* typoGravatar Enrico Tassi2014-09-29
* seems to fix a looping coq-tex (when compiled with camlp4)Gravatar Pierre Boutillier2014-09-18
* Documenting the [Variant] type definition and the [Nonrecursive Elimination S...Gravatar Arnaud Spiwack2014-09-04
* sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.texGravatar Pierre Boutillier2014-09-03
* Update RefMan with respect to new loadpath managementGravatar Pierre Boutillier2014-09-03
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-23 19:56:05 +0000