| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-07-27 | search: Add an output-name-only search option | Clément Pit--Claudel | |
| When set, search results only display symbol names, instead of displaying full terms with types. This is useful when the list of symbols is needed by an external program, in particular for doing completion in IDEs. | |||
| 2015-07-22 | Refman: document Show Universes. | Matthieu Sozeau | |
| 2015-07-22 | Remove obsolete documentation. (Fix bug #4238) | Guillaume Melquiond | |
| 2015-07-18 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-07-08 | Fix documentation of universes. | Matthieu Sozeau | |
| 2015-07-08 | Fix documentation. | Guillaume Melquiond | |
| 2015-07-07 | Document Set/Print Firstorder Solver option. | Matthieu Sozeau | |
| 2015-06-28 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-06-26 | Introduction of a "Undelimit Scope" command, undoing "Delimit Scope" | Lionel Rieg | |
| 2015-06-26 | Typos in my previous edition of the reference manual. | Assia Mahboubi | |
| 2015-06-26 | Some edition in the coq_makefile/_CoqProject section. | Assia Mahboubi | |
| There are still two items I do not undertand fully (the last one about -extra-phony, and the removal of external libraries at make clean time, that I could not reproduce on a toy example. | |||
| 2015-06-26 | Added _CoqProject to the index of the reference manual. | Assia Mahboubi | |
| 2015-06-22 | Merge remote-tracking branch 'forge/v8.5' | Pierre Boutillier | |
| 2015-06-17 | Doc: Workers do check for guardedness before sending proofs back | Enrico Tassi | |
| 2015-05-15 | Turning "Set Regular Subst Tactic" on by default (for 8.6). | Hugo Herbelin | |
| 2015-05-13 | Documenting Set Regular Subst Tactic (though unsure this is worth the | Hugo Herbelin | |
| level of details, and this option should certainly disappear eventually). | |||
| 2015-05-13 | Documenting the Loose Hint Behavior flag. | Pierre-Marie Pédrot | |
| 2015-05-04 | Fix documentation of Redirect | Enrico Tassi | |
| 2015-05-04 | Add a [Redirect] vernacular command | Clément Pit--Claudel | |
| The command [Redirect "filename" (...)] redirects all the output of [(...)] to file "filename.out". This is useful for storing the results of an [Eval compute], for redirecting the results of a large search, for automatically generating traces of interesting developments, and so on. | |||
| 2015-04-17 | Fixing a few typos + some uniformization of writing in doc. | Hugo Herbelin | |
| 2015-04-15 | Documenting the recommandation of toplevel-only commands. | Pierre-Marie Pédrot | |
| 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-01 | 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-03-31 | Fix various typos in documentation | Matěj Grabovský | |
| Closes #57. | |||
| 2015-03-22 | Qed export -> Qed exporting | Enrico Tassi | |
| 2015-03-13 | Fixing #4127 (command for locating exists notation in refman changed). | Hugo Herbelin | |
| 2015-03-11 | admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032) | Enrico Tassi | |
| - no more inconsistent Axiom in the Prelude - STM can now process Admitted proofs asynchronously - the quick chain can stock "Admitted" jobs in .vio files - the vio2vo step checks the jobs but does not stock the result in the opaque tables (they have no slot) - Admitted emits a warning if the proof is complete - Admitted uses the (partial) proof term to infer section variables used (if not given with Proof using), like for Qed - test-suite: extra line Require TestSuite.admit to each file making use of admit - test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to find TestSuite.admit | |||
| 2015-03-05 | Preprend Fail to all the expected failures in the documentation. | Guillaume Melquiond | |
| This commit also removes comments from Coq examples, as they cause extraneous delayed prompts that clutter the output because coq_tex cannot remove them. Some documentation errors were also fixed in the process, since they are easier to spot now that only unexpected failures stand out. | |||
| 2015-03-03 | Typos in doc modules. | Hugo Herbelin | |
| 2015-02-26 | Fixing bug 3099. | Pierre-Marie Pédrot | |
| 2015-02-23 | Fixed doc of fresh (was already outdated before fixing #3233). | Pierre Courtieu | |
| 2015-02-17 | Remove Whelp commands. | Maxime Dénès | |
| Although these commands were never deprecated, they have been unusable for some time now, since they send requests to an Italian server which is no longer alive. | |||
| 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-16 | Documenting "induction t in ctx" when ctx contains an hyp not mentioning t. | Hugo Herbelin | |
| 2015-02-14 | Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior | Enrico Tassi | |
| Of course such proofs cannot be processed asynchronously | |||
| 2015-02-14 | dependent destruction: Fix (part of) bug #3961, by fixing dependent * | Matthieu Sozeau | |
| generalizing * which was broken since 8.4. | |||
| 2015-02-12 | 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-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-05 | Fix some documentation typos. | Guillaume Melquiond | |
| 2015-01-29 | Fix index of reference manual. | Guillaume Melquiond | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |