aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-12-02Merge remote-tracking branch 'github/pr/371' into v8.6Maxime Dénès
Was PR#371: Update dev/doc/changes with things about mem_named_context
2016-12-02Merge remote-tracking branch 'github/pr/364' into v8.6Maxime Dénès
Was PR#364: Add missing label. Fixes broken ref.
2016-12-02Merge remote-tracking branch 'github/pr/382' into v8.6Maxime Dénès
Was PR#382: [merlin] Adjust merlin for ide.
2016-11-30[merlin] Adjust merlin for ide.Emilio Jesus Gallego Arias
2016-11-30Fix #5183 - Two CoqIDE crash errorsMaxime Dénès
When opening a file without extension, an uncaught exception was occurring. Note that this fix is not complete, since the "Compile Buffer" command still fails. This is because of a limitation of coqc which appends the ".v" extension to its argument even if it already existed (and even if it doesn't exist with the extension!).
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
We introduce a bit of compatibility parsing code to print deprecation warnings.
2016-11-29STM: cur_id must be invalid if an error occurs (fix #5191)Enrico Tassi
Line erroneously removed in 17f3346c
2016-11-24Fix some documentation typos.Guillaume Melquiond
Note: "dependant" does exist, but it is a noun and it means a person that is somehow financially dependent on someone else.
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
If the result had its 30th bit set, then all the high part of the result on a 64-bit architecture would end up being set, thus breaking subsequent computations. This patch also fixes the incorrectly parenthesized definition of uint32_of_value, which by luck was never misused.
2016-11-22Properly parenthesize "ltac:" arguments (bug #5169).Guillaume Melquiond
2016-11-21(v8.6) Update dev/doc/changes with things about mem_named_contextJason Gross
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 ↵Guillaume Melquiond
#3339).
2016-11-18Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"Maxime Dénès
This reverts commit b00e039b957b8428c21faec5c76f3a3484cde2cf, reversing changes made to ca9e00ff9b2a8ee17430398a5e0bef2345c39341. It turns out that calling from fake_ide the STM commands that were removed by this PR requires an extension of the XML protocol. So postponing the integration.
2016-11-18Revert "fake_ide: use the now available Status XML message"Maxime Dénès
This reverts commit 81c9fa0de99400b51c029cdbd1519b4f724e320a.
2016-11-17Add missing label. Fixes broken ref.Théo Zimmermann
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
Was PR#360: [stm] Remove STM-related vernaculars
2016-11-17Merge commit '633ed9c' into v8.6Maxime Dénès
Was PR#192: Add test suite files for 4700-4785
2016-11-17Add test suite files for 4700-4785Jason Gross
I didn't add any test-cases for timing-based bugs (4707, 4768, 4776, 4777, 4779, 4783), nor CoqIDE bugs (4700, 4751, 4752, 4756), nor bugs about printing (4709, 4711, 4720, 4723, 4734, 4736, 4738, 4741, 4743, 4748, 4749, 4750, 4757, 4758, 4765, 4784). I'm not sure what to do with 4712, 4714, 4732, 4740.
2016-11-17[stm] Remove STM-related vernacularsEmilio Jesus Gallego Arias
I think these commands never make a lot of sense on scripts other than debugging and we have better methods now. The last remaining command, used for the tty emulation has been renamed to VtBack, but it should go away at some point too once the legacy interfaces are removed.
2016-11-17Merge remote-tracking branch 'github/pr/362' into v8.6Maxime Dénès
Was PR#362: Revert another part of a477dc in good measure
2016-11-16Minor debug printing bug,Matthieu Sozeau
Hit by OCaml's "if then else" with no "end" once more
2016-11-16Revert more of a477dc for good measureMatthieu Sozeau
We stop failing automatically on non-declared-class nested or toplevel subgoals as in 8.5, instead of the previous a477dc behavior of shelving those goals and failing if shelved goals remained at the end of resolution. It means typeclass resolution during refinement is closer to all:typeclasses eauto. Hints in typeclass_instances for non-declared classes can be used during resolution of _nested_ subgoals when it is fired from type-inference, toplevel goals considered in this case are still only classes (as in 8.5 and before). The code that triggers the restriction to only declared class subgoals is commented. Revert changes to test-suite, adding test for #5203, #5198 is fixed too. Add corresponding tests in the test-suite (that will break if we, e.g. disallow non-class subgoals) and update the refman accordingly.
2016-11-16Merge remote-tracking branch 'github/pr/361' into v8.6Maxime Dénès
Was PR#361: [doc] Mention XML protocol on changes.
2016-11-16[doc] Mention XML protocol on changes.Emilio Jesus Gallego Arias
It may be worth it, also added a note about file reorganization.
2016-11-15Merge remote-tracking branch 'github/pr/358' into v8.6Maxime Dénès
Was PR#358: Revert part of a477dc, disallow_shelved
2016-11-15Revert part of a477dc, disallow_shelvedMatthieu Sozeau
In only_classes mode we do not try to implement a stricter semantics for shelved goals in 8.6. Leaving this for 8.7. Update the documentation as well. Remove a spurious printf call as well. Fix test-suite now that shelved goals are allowed
2016-11-14Remove README.win until we come up with new instructions.Maxime Dénès
The recommended way to install Coq under windows is anyway to use the precompiled installer.
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
We could not produce an exhaustive list of such fixes, and the usefulness of such a list is not clear.
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
Was PR#347: Fix performance problem in pose proof
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
Was PR#348: Credits for 8.6
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
Was PR#339: Documenting type class options, typeclasses eauto
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 10:46:11 +0000