aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman
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
* 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
* 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
* Fix some broken Coq scripts in the documentation.Gravatar Guillaume Melquiond2015-07-30
* 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
* 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
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 05:41:13 +0000