aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-16lib/Unicodetable: Update. This code has been generated from the latestYann Régis-Gianas
Unicode tables using UUCD, an OCaml library to parse the official Unicode tables.
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-10Remove unused feedback_content: GoalsCJ Bell
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-08Introducing a new EConstr.t type to perform the nf_evar operation on demand.Pierre-Marie Pédrot
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-08Complete a truncated commentArnaud Spiwack
Introduce by myself, I'm afraid, in #308. Noticed by PMP during the review, but I forgot to fix it before merge.
2016-11-08tclDISPATCH: more informative error messageArnaud Spiwack
"expected _n_ tactics" -> "exected _n_ tactics, was given _k_". Also affect other similar tacticals from `Proofview`. I used that for debugging once, I thought I might as well propose it for mergeing.
2016-11-07Ordering search: memoise relevance metricArnaud Spiwack
Recalculating the metric all the time was proving costly (it was obvious even on small queries).
2016-11-07Refine the relevance measureArnaud Spiwack
Having more disctinc symbols incurs a penalty.
2016-11-07Sort search results by relevanceArnaud Spiwack
This orders the results of search commands (such as `Search`, `SearchAbout`, …) according to a "relevance" metric to minimise. In this minimal version, the metric is the size of the displayed term.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-29 19:51:38 +0000