aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-07-29Fixing bug #3811: "Universe annotations confused inside generalizing binders".Pierre-Marie Pédrot
2015-07-28Adding a test for bug #4280.Pierre-Marie Pédrot
2015-07-28Fix for bug #4280: "decide equality produces terms that don't compute well".Pierre-Marie Pédrot
2015-07-28Make coq-tex aware of lines ending with "}", so as to fix the FAQ.Guillaume Melquiond
2015-07-28Reset a dangling proof in the FAQ.Guillaume Melquiond
2015-07-28Fixing bug #4281: Better escaping of XML attributes.Pierre-Marie Pédrot
2015-07-28ShowScript: as 8.4 w.r.t. unnamed proofs and non tactic vernacs (fix #4308)Enrico Tassi
2015-07-28Updating test-suite for #3510.Pierre-Marie Pédrot
2015-07-28Tests for bugs #3509 and #3510.Pierre-Marie Pédrot
2015-07-28Fixing bug #3509 and #3510 (anomalies in "tactics/term_dnet.ml").Pierre-Marie Pédrot
2015-07-28Use open_utf8_file_in for opening files in the IDE. (Fix bug #2874)Guillaume Melquiond
2015-07-27Test for bug #2243.Pierre-Marie Pédrot
2015-07-27Fixing #4305 (compatibility wrt 8.4 in not interpreting anHugo Herbelin
2015-07-27Slightly improving line break formatting in Info command.Hugo Herbelin
2015-07-27Improving over 26aa224293 in reporting unexpected error during scheme creation.Hugo Herbelin
2015-07-27Fixing bug #3736 (anomaly instead of error/warning/silence onHugo Herbelin
2015-07-27Output test for bug #2169.Pierre-Marie Pédrot
2015-07-27Fixing bug #2169:Pierre-Marie Pédrot
2015-07-26Regenerate the axiom figure of the FAQ.Guillaume Melquiond
2015-07-26Remove obsolete question about eta-conversion.Guillaume Melquiond
2015-07-24Using maps and sets instead of lists in coqdep.Pierre-Marie Pédrot
2015-07-24Fixing bug #4265: "coqdep does not handle From ... Require" for good.Pierre-Marie Pédrot
2015-07-23Silence `which`Jason Gross
2015-07-23adding a missing case for printing zippers.Gregory Malecha
2015-07-23a small amount of documentation on the virtual machine.Gregory Malecha
2015-07-22Removing the G_xml module again.Pierre-Marie Pédrot
2015-07-22Refman: document Show Universes.Matthieu Sozeau
2015-07-22test-suite: add test for bug# 3743.Matthieu Sozeau
2015-07-22Extraction: fix primitive projection extraction.Matthieu Sozeau
2015-07-22Fix incomplete pattern-matching.Matthieu Sozeau
2015-07-22Remove obsolete documentation. (Fix bug #4238)Guillaume Melquiond
2015-07-21Fixing bug #4303: Anomaly: Uncaught exception Invalid_argument.Pierre-Marie Pédrot
2015-07-16Refining 71def2f8 on too strong occur-check limiting evar-evarHugo Herbelin
2015-07-16Slight improvement in naming anonymous variables in error messages:Hugo Herbelin
2015-07-16Fixing #4177 (find_projectable was liable to ask to instantiate an evar twice).Hugo Herbelin
2015-07-16Remove old test file for #3819 (now fixed).Maxime Dénès
2015-07-16Fixing bug #4240 (closure_of_filter was not ensuring refinement ofHugo Herbelin
2015-07-16Test file for #3819.Maxime Dénès
2015-07-16Fix universe instantiation with canonical structures.Maxime Dénès
2015-07-16Modules: fix bug #4294Matthieu Sozeau
2015-07-16Continuing 93579407, spotting other potential sources of anomalyHugo Herbelin
2015-07-16Fixing anomaly #3743 while printing an error message involving evar constraints.Hugo Herbelin
2015-07-15Univs/Inductive: fix typechecking of casesMatthieu Sozeau
2015-07-14STM: fix a "exn with no safe id attached" error on a failing queryEnrico Tassi
2015-07-12Updating checksum in checker (9c732a5cc continued).Hugo Herbelin
2015-07-11CoqIDE: recenter on backtrack (Close: #4277)Enrico Tassi
2015-07-10Rewording about how to upgrade on failing calls to constructor.Hugo Herbelin
2015-07-10Unused variables reported by OCaml.Hugo Herbelin
2015-07-10Continuing handling of NoCoercion after df6e64fd28 and 4944b5e72.Hugo Herbelin
2015-07-10Option -type-in-type: added support in checker and making it contaminatingHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 05:57:16 +0000