aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-11-30Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-30Fix #5183 - Two CoqIDE crash errorsMaxime Dénès
2016-11-30Update copyright on documentation cover.Maxime Dénès
2016-11-30Fix #5174: Underinformative syntax error messages in the new arguments syntaxMaxime Dénès
2016-11-29STM: cur_id must be invalid if an error occurs (fix #5191)Enrico Tassi
2016-11-24Fix some documentation typos.Guillaume Melquiond
2016-11-24Lazily load constants in micromega (bug #5134).Guillaume Melquiond
2016-11-24Fix some documentation typos.Guillaume Melquiond
2016-11-24Fix incorrect long multiplication in the VM.Guillaume Melquiond
2016-11-22Fix locality of "Hint Resolve <->" (bug #5189).Guillaume Melquiond
2016-11-22Properly parenthesize "ltac:" arguments (bug #5169).Guillaume Melquiond
2016-11-21Remove spurious spaces in merlin file generated by coq_makefile (bug #5213).Guillaume Melquiond
2016-11-21Stop parsing -compat-notations options, which are no longer supported (bug #3...Guillaume Melquiond
2016-11-19Tests for info/debug auto/eauto.Hugo Herbelin
2016-11-18Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-18Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"Maxime Dénès
2016-11-18Revert "fake_ide: use the now available Status XML message"Maxime Dénès
2016-11-17fake_ide: use the now available Status XML messageEnrico Tassi
2016-11-17Merge remote-tracking branch 'github/pr/360' into v8.6Maxime Dénès
2016-11-17Merge commit '633ed9c' into v8.6Maxime Dénès
2016-11-17Add test suite files for 4700-4785Jason Gross
2016-11-17[stm] Remove STM-related vernacularsEmilio Jesus Gallego Arias
2016-11-17Merge remote-tracking branch 'github/pr/362' into v8.6Maxime Dénès
2016-11-16Minor debug printing bug,Matthieu Sozeau
2016-11-16Revert more of a477dc for good measureMatthieu Sozeau
2016-11-16Merge remote-tracking branch 'github/pr/361' into v8.6Maxime Dénès
2016-11-16[doc] Mention XML protocol on changes.Emilio Jesus Gallego Arias
2016-11-15Merge remote-tracking branch 'github/pr/358' into v8.6Maxime Dénès
2016-11-15Revert part of a477dc, disallow_shelvedMatthieu Sozeau
2016-11-14Remove README.win until we come up with new instructions.Maxime Dénès
2016-11-14Set version number to 8.6beta1.Maxime Dénès
2016-11-14Remove the list of bug fixes from CHANGES.Maxime Dénès
2016-11-14Fix bug in warnings: -w foo was silent when foo did not exist.Maxime Dénès
2016-11-14Do not mention "none" in warnings doc, as it is there for compatibility.Maxime Dénès
2016-11-11Coqide: fixing default local links for refman and stdlib.Hugo Herbelin
2016-11-11Making explicit that a result is discarded (ocaml warning).Hugo Herbelin
2016-11-10Move OSX script.Maxime Dénès
2016-11-10Add Michael Soegtrop's new script to build windows installer.Maxime Dénès
2016-11-10Remove old windows build scripts.Maxime Dénès
2016-11-10Update CHANGES and credits for 8.6beta1.Maxime Dénès
2016-11-10Updating a comment in test-suite.Hugo Herbelin
2016-11-08Merge commit 'b385fbb' into v8.6Maxime Dénès
2016-11-08Use pf_get_type_of to avoid blowup in pose proof of large proof termsMatthieu Sozeau
2016-11-08Merge remote-tracking branch 'github/pr/348' into v8.6Maxime Dénès
2016-11-08Update documentation of Arguments after recent changes.Maxime Dénès
2016-11-08Rewording from EnricoMatthieu Sozeau
2016-11-07After Emilio's comment.Matthieu Sozeau
2016-11-07Merge remote-tracking branch 'github/pr/339' into v8.6Maxime Dénès
2016-11-07Mention notypeclasses refine in CHANGESMatthieu Sozeau
2016-11-07CHANGES for this branch.Matthieu Sozeau