aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
| * Cosmetic changes in evarconv.ml: hopefully more regular form andGravatar Hugo Herbelin2015-08-02
| * Cosmetic changes in evarconv.ml: hopefully using better self-documenting names.Gravatar Hugo Herbelin2015-08-02
| * Evarconv.ml: small cut-elimination, saving useless zip.Gravatar Hugo Herbelin2015-08-02
| * Cosmetic in evarconv.ml: naming a local function for better readibility.Gravatar Hugo Herbelin2015-08-02
| * Adding a notation { x & P } for { x : _ & P }.Gravatar Hugo Herbelin2015-08-02
| * A patch renaming equal into eq in the module dealing withGravatar Hugo Herbelin2015-08-02
| * Adding eq/compare/hash for syntactic view atGravatar Hugo Herbelin2015-08-02
| * Give a way to control if the decidable-equality schemes are built likeGravatar Hugo Herbelin2015-08-02
| * Removing the generalization of the body of inductive schemes fromGravatar Hugo Herbelin2015-08-02
| * Fixing #4221 (interpreting bound variables using ltac env was possiblyGravatar Hugo Herbelin2015-08-02
| * Granting Jason's request for an ad hoc compatibility option onGravatar Hugo Herbelin2015-08-02
| * Documenting change of behavior of apply when the lemma is a tuple andGravatar Hugo Herbelin2015-08-02
| * For convenience, making yes and on, and no and off synonymous inGravatar Hugo Herbelin2015-08-02
| * Fix typos in the Extraction part of the reference manual.Gravatar Guillaume Melquiond2015-07-31
| * Fix typos in the Micromega part of the reference manual.Gravatar Guillaume Melquiond2015-07-31
| * Improve the table of content of the reference manual.Gravatar Guillaume Melquiond2015-07-31
| * Remove some outdated files and fix permissions.Gravatar Guillaume Melquiond2015-07-31
| * Followup of 9f81b58551.Gravatar Pierre-Marie Pédrot2015-07-30
| * STM: make multiple, admitted, nested proofs work (fix #4314)Gravatar Enrico Tassi2015-07-30
| * STM: emit a warning when a QED/Admitted proof contains a nested lemmaGravatar Enrico Tassi2015-07-30
| * STM: fix backtrack in presence of nested, immediate, proofsGravatar Enrico Tassi2015-07-30
| * STM: remove assertion not being true for nested, immediate, proofs (#4313)Gravatar Enrico Tassi2015-07-30
| * Test file for bug #4289 (buggy hash-consing of kernel name pairsGravatar Hugo Herbelin2015-07-30
| * Fixing bug #4289 (hash-consing only user part of constant notGravatar Hugo Herbelin2015-07-30
| * A printer for printing constants of the env (maybe useful when there are not ...Gravatar Hugo Herbelin2015-07-30
| * Avoid suggesting elim and decompose in the FAQ.Gravatar Guillaume Melquiond2015-07-30
| * Remove some output of Qed in the FAQ.Gravatar Guillaume Melquiond2015-07-30
| * Fix some broken Coq scripts in the documentation.Gravatar Guillaume Melquiond2015-07-30
| * Fix width of underscore in coq_tex output.Gravatar Guillaume Melquiond2015-07-30
| * Fix broken regexp.Gravatar Guillaume Melquiond2015-07-30
| * Remove unused variables.Gravatar Guillaume Melquiond2015-07-30
| * Remove usage of Printexc.catch in the tools, as it is deprecated since 2001.Gravatar Guillaume Melquiond2015-07-30
| * Make coq-tex more robust with respect to the (non-)command on the last line.Gravatar Guillaume Melquiond2015-07-29
| * Remove empty commands from the output of coq-tex.Gravatar Guillaume Melquiond2015-07-29
| * Improve the FAQ a bit.Gravatar Guillaume Melquiond2015-07-29
| * Rewrite the main loop of coq-tex.Gravatar Guillaume Melquiond2015-07-29
| * Adding test for bug #3779.Gravatar Pierre-Marie Pédrot2015-07-29
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-07-29
|\|
| * Fixing some English misspelling.Gravatar Hugo Herbelin2015-07-29
| * Fixing what seems to be a typo.Gravatar Hugo Herbelin2015-07-29
| * Fixing bug #3811: "Universe annotations confused inside generalizing binders".Gravatar Pierre-Marie Pédrot2015-07-29
| * Adding a test for bug #4280.Gravatar Pierre-Marie Pédrot2015-07-28
| * Fix for bug #4280: "decide equality produces terms that don't compute well".Gravatar Pierre-Marie Pédrot2015-07-28
| * Make coq-tex aware of lines ending with "}", so as to fix the FAQ.Gravatar Guillaume Melquiond2015-07-28
| * Reset a dangling proof in the FAQ.Gravatar Guillaume Melquiond2015-07-28
| * Fixing bug #4281: Better escaping of XML attributes.Gravatar Pierre-Marie Pédrot2015-07-28
| * ShowScript: as 8.4 w.r.t. unnamed proofs and non tactic vernacs (fix #4308)Gravatar Enrico Tassi2015-07-28
| * Updating test-suite for #3510.Gravatar Pierre-Marie Pédrot2015-07-28
| * Tests for bugs #3509 and #3510.Gravatar Pierre-Marie Pédrot2015-07-28
| * Fixing bug #3509 and #3510 (anomalies in "tactics/term_dnet.ml").Gravatar Pierre-Marie Pédrot2015-07-28
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-31 21:44:57 +0000