index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
doc
Commit message (
Expand
)
Author
Age
*
Doc: Workers do check for guardedness before sending proofs back
Enrico Tassi
2015-06-17
*
Documenting Set Regular Subst Tactic (though unsure this is worth the
Hugo Herbelin
2015-05-13
*
Documenting the Loose Hint Behavior flag.
Pierre-Marie Pédrot
2015-05-13
*
Fix documentation of Redirect
Enrico Tassi
2015-05-04
*
Add a [Redirect] vernacular command
Clément Pit--Claudel
2015-05-04
*
Fixing a few typos + some uniformization of writing in doc.
Hugo Herbelin
2015-04-17
*
Documenting the recommandation of toplevel-only commands.
Pierre-Marie Pédrot
2015-04-15
*
Fix compilation of documentation broken by the addition of MMapAVL.
Guillaume Melquiond
2015-04-02
*
Make sure that hyperref creates the proper links to the documentation indexes.
Guillaume Melquiond
2015-04-02
*
Fix documentation of -R and -Q.
Guillaume Melquiond
2015-04-02
*
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
*
Fix various typos in documentation
Matěj Grabovský
2015-03-31
*
Qed export -> Qed exporting
Enrico Tassi
2015-03-22
*
Index MMaps files, otherwise documentation cannot be built. (Fix for bug #4107)
Guillaume Melquiond
2015-03-21
*
Fixing #4127 (command for locating exists notation in refman changed).
Hugo Herbelin
2015-03-13
*
admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)
Enrico Tassi
2015-03-11
*
Preprend Fail to all the expected failures in the documentation.
Guillaume Melquiond
2015-03-05
*
Typos in doc modules.
Hugo Herbelin
2015-03-03
*
Fixing bug 3099.
Pierre-Marie Pédrot
2015-02-26
*
Fixed doc of fresh (was already outdated before fixing #3233).
Pierre Courtieu
2015-02-23
*
Remove Whelp commands.
Maxime Dénès
2015-02-17
*
Separate index for vernacular options.
Maxime Dénès
2015-02-17
*
Remove documentation of non-existing Show Implicits command.
Maxime Dénès
2015-02-17
*
Remove non-existing Tactic Definition command from index.
Maxime Dénès
2015-02-17
*
Fix sentence that was cut in doc of Local Set.
Maxime Dénès
2015-02-17
*
Documenting "induction t in ctx" when ctx contains an hyp not mentioning t.
Hugo Herbelin
2015-02-16
*
Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior
Enrico Tassi
2015-02-14
*
dependent destruction: Fix (part of) bug #3961, by fixing dependent *
Matthieu Sozeau
2015-02-14
*
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
*
Avoid html markup inside tex files and fix url.
Guillaume Melquiond
2015-02-10
*
A few refinements in whodidwhat 8.4.
Hugo Herbelin
2015-02-10
*
Add section numbering to the refman PDF. (Fix for bug #2365)
Guillaume Melquiond
2015-02-10
*
Prevent Latex from messing with backticks. (Fix for bug #3871)
Guillaume Melquiond
2015-02-10
*
Fix documentation of generalize. (Fix for bug #4015)
Guillaume Melquiond
2015-02-10
*
Fix some documentation typo.
Guillaume Melquiond
2015-02-10
*
Fix some documentation typos.
Guillaume Melquiond
2015-02-05
*
Fix index of reference manual.
Guillaume Melquiond
2015-01-29
*
Remove spurious "Loading ML file" and "<W> Grammar extension" from the refere...
Guillaume Melquiond
2015-01-29
*
Remove some "Warning:" from the reference manual.
Guillaume Melquiond
2015-01-29
*
Fix some typos in the documentation.
Guillaume Melquiond
2015-01-29
*
Fix some broken Coq scripts in the reference manual.
Guillaume Melquiond
2015-01-29
*
Doc: Overfull lines in chapter on Canonical Structures.
Hugo Herbelin
2015-01-27
*
Doc: Fixing some compilation problems with chapter Canonical
Hugo Herbelin
2015-01-24
*
Reference Manual: Documenting new printing of evars and new effect of
Hugo Herbelin
2015-01-24
*
Reference Manual/Credits: expand the paragraph on the new proof engine to mat...
Arnaud Spiwack
2015-01-21
*
Reference Manual/Credits: native compute is a major contribution.
Arnaud Spiwack
2015-01-21
*
Reference manual/Credits: populate the "various smaller-scale improvements" p...
Arnaud Spiwack
2015-01-21
[next]