aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-07-31Improve the table of content of the reference manual.Guillaume Melquiond
2015-07-31Remove some outdated files and fix permissions.Guillaume Melquiond
2015-07-30Followup of 9f81b58551.Pierre-Marie Pédrot
2015-07-30STM: make multiple, admitted, nested proofs work (fix #4314)Enrico Tassi
2015-07-30STM: emit a warning when a QED/Admitted proof contains a nested lemmaEnrico Tassi
2015-07-30STM: fix backtrack in presence of nested, immediate, proofsEnrico Tassi
2015-07-30STM: remove assertion not being true for nested, immediate, proofs (#4313)Enrico Tassi
2015-07-30Test file for bug #4289 (buggy hash-consing of kernel name pairsHugo Herbelin
2015-07-30Fixing bug #4289 (hash-consing only user part of constant notHugo Herbelin
2015-07-30A printer for printing constants of the env (maybe useful when there are not ...Hugo Herbelin
2015-07-30Avoid suggesting elim and decompose in the FAQ.Guillaume Melquiond
2015-07-30Remove some output of Qed in the FAQ.Guillaume Melquiond
2015-07-30Fix some broken Coq scripts in the documentation.Guillaume Melquiond
2015-07-30Fix width of underscore in coq_tex output.Guillaume Melquiond
2015-07-30Fix broken regexp.Guillaume Melquiond
2015-07-30Remove unused variables.Guillaume Melquiond
2015-07-30Remove usage of Printexc.catch in the tools, as it is deprecated since 2001.Guillaume Melquiond
2015-07-29Make coq-tex more robust with respect to the (non-)command on the last line.Guillaume Melquiond
2015-07-29Remove empty commands from the output of coq-tex.Guillaume Melquiond
2015-07-29Improve the FAQ a bit.Guillaume Melquiond
2015-07-29Rewrite the main loop of coq-tex.Guillaume Melquiond
2015-07-29Adding test for bug #3779.Pierre-Marie Pédrot
2015-07-29Fixing some English misspelling.Hugo Herbelin
2015-07-29Fixing what seems to be a typo.Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 11:46:15 +0000