aboutsummaryrefslogtreecommitdiff
path: root/doc/refman
AgeCommit message (Expand)Author
2015-07-27search: Add an output-name-only search optionClément Pit--Claudel
2015-07-22Refman: document Show Universes.Matthieu Sozeau
2015-07-22Remove obsolete documentation. (Fix bug #4238)Guillaume Melquiond
2015-07-18Merge branch 'v8.5'Pierre-Marie Pédrot
2015-07-08Fix documentation of universes.Matthieu Sozeau
2015-07-08Fix documentation.Guillaume Melquiond
2015-07-07Document Set/Print Firstorder Solver option.Matthieu Sozeau
2015-06-28Merge branch 'v8.5'Pierre-Marie Pédrot
2015-06-26Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Lionel Rieg
2015-06-26Typos in my previous edition of the reference manual.Assia Mahboubi
2015-06-26Some edition in the coq_makefile/_CoqProject section.Assia Mahboubi
2015-06-26Added _CoqProject to the index of the reference manual.Assia Mahboubi
2015-06-22Merge remote-tracking branch 'forge/v8.5'Pierre Boutillier
2015-06-17Doc: Workers do check for guardedness before sending proofs backEnrico Tassi
2015-05-15Turning "Set Regular Subst Tactic" on by default (for 8.6).Hugo Herbelin
2015-05-13Documenting Set Regular Subst Tactic (though unsure this is worth theHugo Herbelin
2015-05-13Documenting the Loose Hint Behavior flag.Pierre-Marie Pédrot
2015-05-04Fix documentation of RedirectEnrico Tassi
2015-05-04Add a [Redirect] vernacular commandClément Pit--Claudel
2015-04-17Fixing a few typos + some uniformization of writing in doc.Hugo Herbelin
2015-04-15Documenting the recommandation of toplevel-only commands.Pierre-Marie Pédrot
2015-04-02Make sure that hyperref creates the proper links to the documentation indexes.Guillaume Melquiond
2015-04-02Fix documentation of -R and -Q.Guillaume Melquiond
2015-04-01Fixing a few typos + some uniformization of writing in doc.Hugo Herbelin
2015-04-01More clarifications on loadpaths.Pierre-Marie Pédrot
2015-04-01Documenting "From * Require *" and clearing a bit the loadpath chapter.Pierre-Marie Pédrot
2015-03-31Fix various typos in documentationMatěj Grabovský
2015-03-22Qed export -> Qed exportingEnrico Tassi
2015-03-13Fixing #4127 (command for locating exists notation in refman changed).Hugo Herbelin
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2015-03-05Preprend Fail to all the expected failures in the documentation.Guillaume Melquiond
2015-03-03Typos in doc modules.Hugo Herbelin
2015-02-26Fixing bug 3099.Pierre-Marie Pédrot
2015-02-23Fixed doc of fresh (was already outdated before fixing #3233).Pierre Courtieu
2015-02-17Remove Whelp commands.Maxime Dénès
2015-02-17Separate index for vernacular options.Maxime Dénès
2015-02-17Remove documentation of non-existing Show Implicits command.Maxime Dénès
2015-02-17Remove non-existing Tactic Definition command from index.Maxime Dénès
2015-02-17Fix sentence that was cut in doc of Local Set.Maxime Dénès
2015-02-16Documenting "induction t in ctx" when ctx contains an hyp not mentioning t.Hugo Herbelin
2015-02-14Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorEnrico Tassi
2015-02-14dependent destruction: Fix (part of) bug #3961, by fixing dependent *Matthieu Sozeau
2015-02-12Fix typos about .vio files (thanks Arthur for spotting them)Enrico Tassi
2015-02-12Make clearer that "Remove Printing Let" does not influence destructuring let.Guillaume Melquiond
2015-02-10Add section numbering to the refman PDF. (Fix for bug #2365)Guillaume Melquiond
2015-02-10Prevent Latex from messing with backticks. (Fix for bug #3871)Guillaume Melquiond
2015-02-10Fix documentation of generalize. (Fix for bug #4015)Guillaume Melquiond
2015-02-10Fix some documentation typo.Guillaume Melquiond
2015-02-05Fix some documentation typos.Guillaume Melquiond
2015-01-29Fix index of reference manual.Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 15:21:01 +0000