aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* 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
* 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
* Use open_utf8_file_in for opening files in the IDE. (Fix bug #2874)Gravatar Guillaume Melquiond2015-07-28
* Test for bug #2243.Gravatar Pierre-Marie Pédrot2015-07-27
* Fixing #4305 (compatibility wrt 8.4 in not interpreting anGravatar Hugo Herbelin2015-07-27
* Slightly improving line break formatting in Info command.Gravatar Hugo Herbelin2015-07-27
* Improving over 26aa224293 in reporting unexpected error during scheme creation.Gravatar Hugo Herbelin2015-07-27
* Fixing bug #3736 (anomaly instead of error/warning/silence onGravatar Hugo Herbelin2015-07-27
* Output test for bug #2169.Gravatar Pierre-Marie Pédrot2015-07-27
* Fixing bug #2169:Gravatar Pierre-Marie Pédrot2015-07-27
* Regenerate the axiom figure of the FAQ.Gravatar Guillaume Melquiond2015-07-26
* Remove obsolete question about eta-conversion.Gravatar Guillaume Melquiond2015-07-26
* Using maps and sets instead of lists in coqdep.Gravatar Pierre-Marie Pédrot2015-07-24
* Fixing bug #4265: "coqdep does not handle From ... Require" for good.Gravatar Pierre-Marie Pédrot2015-07-24
* Silence `which`Gravatar Jason Gross2015-07-23
* adding a missing case for printing zippers.Gravatar Gregory Malecha2015-07-23
* a small amount of documentation on the virtual machine.Gravatar Gregory Malecha2015-07-23
* Removing the G_xml module again.Gravatar Pierre-Marie Pédrot2015-07-22
* Refman: document Show Universes.Gravatar Matthieu Sozeau2015-07-22
* test-suite: add test for bug# 3743.Gravatar Matthieu Sozeau2015-07-22
* Extraction: fix primitive projection extraction.Gravatar Matthieu Sozeau2015-07-22
* Fix incomplete pattern-matching.Gravatar Matthieu Sozeau2015-07-22
* Remove obsolete documentation. (Fix bug #4238)Gravatar Guillaume Melquiond2015-07-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 04:21:08 +0000