Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Introduction of a "Undelimit Scope" command, undoing "Delimit Scope" | 2015-06-26 | |
| | |||
* | Typos in my previous edition of the reference manual. | 2015-06-26 | |
| | |||
* | Some edition in the coq_makefile/_CoqProject section. | 2015-06-26 | |
| | | | | | | 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. | ||
* | Added _CoqProject to the index of the reference manual. | 2015-06-26 | |
| | |||
* | Doc: Workers do check for guardedness before sending proofs back | 2015-06-17 | |
| | |||
* | Documenting Set Regular Subst Tactic (though unsure this is worth the | 2015-05-13 | |
| | | | | | level of details, and this option should certainly disappear eventually). | ||
* | Documenting the Loose Hint Behavior flag. | 2015-05-13 | |
| | |||
* | Fix documentation of Redirect | 2015-05-04 | |
| | |||
* | Add a [Redirect] vernacular command | 2015-05-04 | |
| | | | | | | | 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. | ||
* | Fixing a few typos + some uniformization of writing in doc. | 2015-04-17 | |
| | |||
* | Documenting the recommandation of toplevel-only commands. | 2015-04-15 | |
| | |||
* | Fix compilation of documentation broken by the addition of MMapAVL. | 2015-04-02 | |
| | |||
* | Make sure that hyperref creates the proper links to the documentation indexes. | 2015-04-02 | |
| | |||
* | Fix documentation of -R and -Q. | 2015-04-02 | |
| | |||
* | Fixing a few typos + some uniformization of writing in doc. | 2015-04-01 | |
| | |||
* | More clarifications on loadpaths. | 2015-04-01 | |
| | |||
* | Documenting "From * Require *" and clearing a bit the loadpath chapter. | 2015-04-01 | |
| | |||
* | Fix various typos in documentation | 2015-03-31 | |
| | | | | Closes #57. | ||
* | Qed export -> Qed exporting | 2015-03-22 | |
| | |||
* | Index MMaps files, otherwise documentation cannot be built. (Fix for bug #4107) | 2015-03-21 | |
| | |||
* | Fixing #4127 (command for locating exists notation in refman changed). | 2015-03-13 | |
| | |||
* | admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032) | 2015-03-11 | |
| | | | | | | | | | | | | | | | - 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 | ||
* | Preprend Fail to all the expected failures in the documentation. | 2015-03-05 | |
| | | | | | | | 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. | ||
* | Typos in doc modules. | 2015-03-03 | |
| | |||
* | Fixing bug 3099. | 2015-02-26 | |
| | |||
* | Fixed doc of fresh (was already outdated before fixing #3233). | 2015-02-23 | |
| | |||
* | Remove Whelp commands. | 2015-02-17 | |
| | | | | | | 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. | ||
* | Separate index for vernacular options. | 2015-02-17 | |
| | |||
* | Remove documentation of non-existing Show Implicits command. | 2015-02-17 | |
| | |||
* | Remove non-existing Tactic Definition command from index. | 2015-02-17 | |
| | |||
* | Fix sentence that was cut in doc of Local Set. | 2015-02-17 | |
| | |||
* | Documenting "induction t in ctx" when ctx contains an hyp not mentioning t. | 2015-02-16 | |
| | |||
* | Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior | 2015-02-14 | |
| | | | | Of course such proofs cannot be processed asynchronously | ||
* | dependent destruction: Fix (part of) bug #3961, by fixing dependent * | 2015-02-14 | |
| | | | | generalizing * which was broken since 8.4. | ||
* | Fix typos about .vio files (thanks Arthur for spotting them) | 2015-02-12 | |
| | |||
* | Make clearer that "Remove Printing Let" does not influence destructuring let. | 2015-02-12 | |
| | |||
* | Avoid html markup inside tex files and fix url. | 2015-02-10 | |
| | |||
* | A few refinements in whodidwhat 8.4. | 2015-02-10 | |
| | |||
* | Add section numbering to the refman PDF. (Fix for bug #2365) | 2015-02-10 | |
| | |||
* | Prevent Latex from messing with backticks. (Fix for bug #3871) | 2015-02-10 | |
| | |||
* | Fix documentation of generalize. (Fix for bug #4015) | 2015-02-10 | |
| | |||
* | Fix some documentation typo. | 2015-02-10 | |
| | |||
* | Fix some documentation typos. | 2015-02-05 | |
| | |||
* | Fix index of reference manual. | 2015-01-29 | |
| | |||
* | Remove spurious "Loading ML file" and "<W> Grammar extension" from the ↵ | 2015-01-29 | |
| | | | | reference manual. | ||
* | Remove some "Warning:" from the reference manual. | 2015-01-29 | |
| | |||
* | Fix some typos in the documentation. | 2015-01-29 | |
| | |||
* | Fix some broken Coq scripts in the reference manual. | 2015-01-29 | |
| | |||
* | Doc: Overfull lines in chapter on Canonical Structures. | 2015-01-27 | |
| | |||
* | Doc: Fixing some compilation problems with chapter Canonical | 2015-01-24 | |
| | | | | | Structures. Text mode + a "Require Import" in a module which provokes suspect warnings "Exception Not_found". |