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