| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-08-02 | Granting Jason's request for an ad hoc compatibility option on | Hugo Herbelin | |
| considering trivial unifications "?x = t" in tactics working under conjunctions (see #3545). Also updating and fixing wrong comments in test apply.v. | |||
| 2015-07-31 | Fix typos in the Extraction part of the reference manual. | Guillaume Melquiond | |
| In particular, fix the name of all the user contributions. | |||
| 2015-07-31 | Fix typos in the Micromega part of the reference manual. | Guillaume Melquiond | |
| 2015-07-31 | Improve the table of content of the reference manual. | Guillaume Melquiond | |
| Also remove AsyncProofs.tex from the list of preprocessed files, as it is doubtful it will ever contains Coq scripts. | |||
| 2015-07-31 | Remove some outdated files and fix permissions. | Guillaume Melquiond | |
| 2015-07-30 | Avoid suggesting elim and decompose in the FAQ. | Guillaume Melquiond | |
| 2015-07-30 | Remove some output of Qed in the FAQ. | Guillaume Melquiond | |
| 2015-07-30 | Fix some broken Coq scripts in the documentation. | Guillaume Melquiond | |
| 2015-07-29 | Improve the FAQ a bit. | Guillaume Melquiond | |
| 2015-07-29 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-07-28 | Reset a dangling proof in the FAQ. | Guillaume Melquiond | |
| 2015-07-27 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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-26 | Regenerate the axiom figure of the FAQ. | Guillaume Melquiond | |
| The .png was ugly (less than 400px wide) and did not match the content of the .fig file (e.g. presence of '$'). To improve things a bit, text is now rendered by latex. | |||
| 2015-07-26 | Remove obsolete question about eta-conversion. | Guillaume Melquiond | |
| 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 | Fix compilation of documentation broken by the addition of MMapAVL. | Guillaume Melquiond | |
| 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-21 | Index MMaps files, otherwise documentation cannot be built. (Fix for bug #4107) | Guillaume Melquiond | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |