aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* Reference Manual: Applying standard style recommendation about notGravatar Hugo Herbelin2015-10-18
* Fix some typos.Gravatar Guillaume Melquiond2015-10-14
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* Documenting matching under binders.Gravatar Hugo Herbelin2015-10-11
* Fix a few latex errors in documentation of Proof Using (e.g. \tt*).Gravatar Guillaume Melquiond2015-10-10
* Proof using: let-in policy, optional auto-clear, forward closure*Gravatar Enrico Tassi2015-10-08
* Fix typo. (Fix bug #4355)Gravatar Guillaume Melquiond2015-10-04
* Mark the Coq.Compat files for documentation. (Fix bug #4353)Gravatar Guillaume Melquiond2015-10-02
* Fixing error messages about Hint.Gravatar Hugo Herbelin2015-10-02
* Improving reference manual in that auto uses simple apply rather than apply.Gravatar Hugo Herbelin2015-10-02
* Fixing documentation wrt the ctrl-shift-u Unicode input method (see #2013).Gravatar Hugo Herbelin2015-09-30
* Make -load-vernac-object respect the loadpath.Gravatar Guillaume Melquiond2015-09-28
* Documenting how to support some special unicode characters in coqdocGravatar Hugo Herbelin2015-09-26
* Clarifying the doc of coqdoc --utf8 as discussed on coq-club on August 19, 2015.Gravatar Hugo Herbelin2015-09-26
* The -require option now accepts a logical path instead of a physical one.Gravatar Pierre-Marie Pédrot2015-09-25
* Updating the documentation and the toolchain w.r.t. the change in -compile.Gravatar Pierre-Marie Pédrot2015-09-25
* Fixing tutorial.Gravatar Pierre-Marie Pédrot2015-09-21
* typo in refman.Gravatar Pierre Courtieu2015-09-10
* Remove generatable documentation files from repository. (Fix bug #4315)Gravatar Guillaume Melquiond2015-08-17
* Granting Jason's request for an ad hoc compatibility option onGravatar Hugo Herbelin2015-08-02
* Fix typos in the Extraction part of the reference manual.Gravatar Guillaume Melquiond2015-07-31
* Fix typos in the Micromega part of the reference manual.Gravatar Guillaume Melquiond2015-07-31
* Improve the table of content of the reference manual.Gravatar Guillaume Melquiond2015-07-31
* Remove some outdated files and fix permissions.Gravatar Guillaume Melquiond2015-07-31
* Avoid suggesting elim and decompose in the FAQ.Gravatar Guillaume Melquiond2015-07-30
* Remove some output of Qed in the FAQ.Gravatar Guillaume Melquiond2015-07-30
* Fix some broken Coq scripts in the documentation.Gravatar Guillaume Melquiond2015-07-30
* Improve the FAQ a bit.Gravatar Guillaume Melquiond2015-07-29
* Reset a dangling proof in the FAQ.Gravatar Guillaume Melquiond2015-07-28
* Regenerate the axiom figure of the FAQ.Gravatar Guillaume Melquiond2015-07-26
* Remove obsolete question about eta-conversion.Gravatar Guillaume Melquiond2015-07-26
* Refman: document Show Universes.Gravatar Matthieu Sozeau2015-07-22
* Remove obsolete documentation. (Fix bug #4238)Gravatar Guillaume Melquiond2015-07-22
* Fix documentation of universes.Gravatar Matthieu Sozeau2015-07-08
* Fix documentation.Gravatar Guillaume Melquiond2015-07-08
* Document Set/Print Firstorder Solver option.Gravatar Matthieu Sozeau2015-07-07
* Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Gravatar Lionel Rieg2015-06-26
* Typos in my previous edition of the reference manual.Gravatar Assia Mahboubi2015-06-26
* Some edition in the coq_makefile/_CoqProject section.Gravatar Assia Mahboubi2015-06-26
* Added _CoqProject to the index of the reference manual.Gravatar Assia Mahboubi2015-06-26
* Doc: Workers do check for guardedness before sending proofs backGravatar Enrico Tassi2015-06-17
* Documenting Set Regular Subst Tactic (though unsure this is worth theGravatar Hugo Herbelin2015-05-13
* Documenting the Loose Hint Behavior flag.Gravatar Pierre-Marie Pédrot2015-05-13
* Fix documentation of RedirectGravatar Enrico Tassi2015-05-04
* Add a [Redirect] vernacular commandGravatar Clément Pit--Claudel2015-05-04
* Fixing a few typos + some uniformization of writing in doc.Gravatar Hugo Herbelin2015-04-17
* Documenting the recommandation of toplevel-only commands.Gravatar Pierre-Marie Pédrot2015-04-15
* Fix compilation of documentation broken by the addition of MMapAVL.Gravatar Guillaume Melquiond2015-04-02
* Make sure that hyperref creates the proper links to the documentation indexes.Gravatar Guillaume Melquiond2015-04-02
* Fix documentation of -R and -Q.Gravatar Guillaume Melquiond2015-04-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 21:28:07 +0000