aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* 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
* 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
* Fix various typos in documentationGravatar Matěj Grabovský2015-03-31
* Qed export -> Qed exportingGravatar Enrico Tassi2015-03-22
* Index MMaps files, otherwise documentation cannot be built. (Fix for bug #4107)Gravatar Guillaume Melquiond2015-03-21
* Fixing #4127 (command for locating exists notation in refman changed).Gravatar Hugo Herbelin2015-03-13
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* Preprend Fail to all the expected failures in the documentation.Gravatar Guillaume Melquiond2015-03-05
* Typos in doc modules.Gravatar Hugo Herbelin2015-03-03
* Fixing bug 3099.Gravatar Pierre-Marie Pédrot2015-02-26
* Fixed doc of fresh (was already outdated before fixing #3233).Gravatar Pierre Courtieu2015-02-23
* Remove Whelp commands.Gravatar Maxime Dénès2015-02-17
* Separate index for vernacular options.Gravatar Maxime Dénès2015-02-17
* Remove documentation of non-existing Show Implicits command.Gravatar Maxime Dénès2015-02-17
* Remove non-existing Tactic Definition command from index.Gravatar Maxime Dénès2015-02-17
* Fix sentence that was cut in doc of Local Set.Gravatar Maxime Dénès2015-02-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 07:56:45 +0000