aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-11-22Fix locality of "Hint Resolve <->" (bug #5189).Guillaume Melquiond
"Hint Resolve <->" now behaves the same as "Hint Resolve", in that it uses the same default locality and it accepts locality prefixes.
2016-11-19Tests for info/debug auto/eauto.Hugo Herbelin
This is while waiting for a deeper uniformization of auto, eauto, and typeclasses eauto. Incidentally includes a little fix in harmonizing auto/eauto printing.
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
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-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
2016-11-07Mention notypeclasses refine in CHANGESMatthieu Sozeau
2016-11-07CHANGES for this branch.Matthieu Sozeau
2016-11-07Document two new variants of refineMatthieu Sozeau
They allow to call refine without doing typeclass resolution, allowing to use refine in typeclass hints.
2016-11-07Fixes to compile with ocaml 4.01Matthieu Sozeau
2016-11-07More accurate contributor list.Matthieu Sozeau
Command used: git log v8.5..HEAD --pretty=format:"%an," | sort -k 2 | uniq with some manual postprocessing for login names, particles and multiple first names.
2016-11-07Hugo and Maxime's 2nd pass of commentsMatthieu Sozeau
2016-11-07Merge commit 'e6edb33' into v8.6Maxime Dénès
Was PR#331: Solve_constraints and Set Use Unification Heuristics
2016-11-07Improve formatting of a message in [Arguments].Maxime Dénès
2016-11-07Fix #5181: [Arguments] no longer correctly checks the length of arguments listsMaxime Dénès
2016-11-07Fix #5182: "Arguments names must be distinct." is bogus and underinformativeMaxime Dénès
2016-11-07More explicit name for status of unification constraints.Maxime Dénès
2016-11-06Hugo's commentsMatthieu Sozeau
2016-11-06Maxime's commentsMatthieu Sozeau
2016-11-06Fixes from Enrico's reviewMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 01:36:23 +0000