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