| Age | Commit message (Expand) | Author |
|---|
| 2015-08-02 | Evarconv.ml: small cut-elimination, saving useless zip. | Hugo Herbelin |
| 2015-08-02 | Cosmetic in evarconv.ml: naming a local function for better readibility. | Hugo Herbelin |
| 2015-08-02 | Adding a notation { x & P } for { x : _ & P }. | Hugo Herbelin |
| 2015-08-02 | A patch renaming equal into eq in the module dealing with | Hugo Herbelin |
| 2015-08-02 | Adding eq/compare/hash for syntactic view at | Hugo Herbelin |
| 2015-08-02 | Give a way to control if the decidable-equality schemes are built like | Hugo Herbelin |
| 2015-08-02 | Removing the generalization of the body of inductive schemes from | Hugo Herbelin |
| 2015-08-02 | Fixing #4221 (interpreting bound variables using ltac env was possibly | Hugo Herbelin |
| 2015-08-02 | Granting Jason's request for an ad hoc compatibility option on | Hugo Herbelin |
| 2015-08-02 | Documenting change of behavior of apply when the lemma is a tuple and | Hugo Herbelin |
| 2015-08-02 | For convenience, making yes and on, and no and off synonymous in | Hugo Herbelin |
| 2015-07-31 | Fix typos in the Extraction part of the reference manual. | Guillaume Melquiond |
| 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 |
| 2015-07-31 | Remove some outdated files and fix permissions. | Guillaume Melquiond |
| 2015-07-30 | Followup of 9f81b58551. | Pierre-Marie Pédrot |
| 2015-07-30 | STM: make multiple, admitted, nested proofs work (fix #4314) | Enrico Tassi |
| 2015-07-30 | STM: emit a warning when a QED/Admitted proof contains a nested lemma | Enrico Tassi |
| 2015-07-30 | STM: fix backtrack in presence of nested, immediate, proofs | Enrico Tassi |
| 2015-07-30 | STM: remove assertion not being true for nested, immediate, proofs (#4313) | Enrico Tassi |
| 2015-07-30 | Test file for bug #4289 (buggy hash-consing of kernel name pairs | Hugo Herbelin |
| 2015-07-30 | Fixing bug #4289 (hash-consing only user part of constant not | Hugo Herbelin |
| 2015-07-30 | A printer for printing constants of the env (maybe useful when there are not ... | Hugo Herbelin |
| 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-30 | Fix width of underscore in coq_tex output. | Guillaume Melquiond |
| 2015-07-30 | Fix broken regexp. | Guillaume Melquiond |
| 2015-07-30 | Remove unused variables. | Guillaume Melquiond |
| 2015-07-30 | Remove usage of Printexc.catch in the tools, as it is deprecated since 2001. | Guillaume Melquiond |
| 2015-07-29 | Make coq-tex more robust with respect to the (non-)command on the last line. | Guillaume Melquiond |
| 2015-07-29 | Remove empty commands from the output of coq-tex. | Guillaume Melquiond |
| 2015-07-29 | Improve the FAQ a bit. | Guillaume Melquiond |
| 2015-07-29 | Rewrite the main loop of coq-tex. | Guillaume Melquiond |
| 2015-07-29 | Adding test for bug #3779. | Pierre-Marie Pédrot |
| 2015-07-29 | Fixing some English misspelling. | Hugo Herbelin |
| 2015-07-29 | Fixing what seems to be a typo. | Hugo Herbelin |
| 2015-07-29 | Fixing bug #3811: "Universe annotations confused inside generalizing binders". | Pierre-Marie Pédrot |
| 2015-07-28 | Adding a test for bug #4280. | Pierre-Marie Pédrot |
| 2015-07-28 | Fix for bug #4280: "decide equality produces terms that don't compute well". | Pierre-Marie Pédrot |
| 2015-07-28 | Make coq-tex aware of lines ending with "}", so as to fix the FAQ. | Guillaume Melquiond |
| 2015-07-28 | Reset a dangling proof in the FAQ. | Guillaume Melquiond |
| 2015-07-28 | Fixing bug #4281: Better escaping of XML attributes. | Pierre-Marie Pédrot |
| 2015-07-28 | ShowScript: as 8.4 w.r.t. unnamed proofs and non tactic vernacs (fix #4308) | Enrico Tassi |
| 2015-07-28 | Updating test-suite for #3510. | Pierre-Marie Pédrot |
| 2015-07-28 | Tests for bugs #3509 and #3510. | Pierre-Marie Pédrot |
| 2015-07-28 | Fixing bug #3509 and #3510 (anomalies in "tactics/term_dnet.ml"). | Pierre-Marie Pédrot |
| 2015-07-28 | Use open_utf8_file_in for opening files in the IDE. (Fix bug #2874) | Guillaume Melquiond |
| 2015-07-27 | Test for bug #2243. | Pierre-Marie Pédrot |
| 2015-07-27 | Fixing #4305 (compatibility wrt 8.4 in not interpreting an | Hugo Herbelin |
