| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-11-29 | STM: cur_id must be invalid if an error occurs (fix #5191) | Enrico Tassi | |
| Line erroneously removed in 17f3346c | |||
| 2016-11-24 | Fix 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-24 | Lazily load constants in micromega (bug #5134). | Guillaume Melquiond | |
| 2016-11-24 | Fix some documentation typos. | Guillaume Melquiond | |
| 2016-11-24 | Fix 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-22 | Fix 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-22 | Properly parenthesize "ltac:" arguments (bug #5169). | Guillaume Melquiond | |
| 2016-11-21 | (v8.6) Update dev/doc/changes.txt with HintsResolveEntry changes | Jason Gross | |
| 2016-11-21 | (v8.6) Update dev/doc/changes with things about mem_named_context | Jason Gross | |
| 2016-11-21 | (v8.6) Make a note about wit_constr and Constrarg in dev/doc/changes | Jason Gross | |
| 2016-11-21 | (v8.6) Add example in dev/doc/changes involving Tacmach.project | Jason Gross | |
| 2016-11-21 | Remove spurious spaces in merlin file generated by coq_makefile (bug #5213). | Guillaume Melquiond | |
| 2016-11-21 | Stop parsing -compat-notations options, which are no longer supported (bug ↵ | Guillaume Melquiond | |
| #3339). | |||
| 2016-11-19 | Tests 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-18 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-11-18 | Revert "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-18 | Revert "fake_ide: use the now available Status XML message" | Maxime Dénès | |
| This reverts commit 81c9fa0de99400b51c029cdbd1519b4f724e320a. | |||
| 2016-11-17 | Add missing label. Fixes broken ref. | Théo Zimmermann | |
| 2016-11-17 | fake_ide: use the now available Status XML message | Enrico Tassi | |
| 2016-11-17 | Merge remote-tracking branch 'github/pr/360' into v8.6 | Maxime Dénès | |
| Was PR#360: [stm] Remove STM-related vernaculars | |||
| 2016-11-17 | Merge commit '633ed9c' into v8.6 | Maxime Dénès | |
| Was PR#192: Add test suite files for 4700-4785 | |||
| 2016-11-17 | Add test suite files for 4700-4785 | Jason 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 vernaculars | Emilio 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-17 | Merge remote-tracking branch 'github/pr/362' into v8.6 | Maxime Dénès | |
| Was PR#362: Revert another part of a477dc in good measure | |||
| 2016-11-16 | Minor debug printing bug, | Matthieu Sozeau | |
| Hit by OCaml's "if then else" with no "end" once more | |||
| 2016-11-16 | Revert more of a477dc for good measure | Matthieu 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-16 | lib/Unicodetable: Update. This code has been generated from the latest | Yann Régis-Gianas | |
| Unicode tables using UUCD, an OCaml library to parse the official Unicode tables. | |||
| 2016-11-16 | Merge remote-tracking branch 'github/pr/361' into v8.6 | Maxime 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-15 | Merge remote-tracking branch 'github/pr/358' into v8.6 | Maxime Dénès | |
| Was PR#358: Revert part of a477dc, disallow_shelved | |||
| 2016-11-15 | Revert part of a477dc, disallow_shelved | Matthieu 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-14 | Remove 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-14 | Set version number to 8.6beta1. | Maxime Dénès | |
| 2016-11-14 | Remove 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-14 | Fix bug in warnings: -w foo was silent when foo did not exist. | Maxime Dénès | |
| 2016-11-14 | Do not mention "none" in warnings doc, as it is there for compatibility. | Maxime Dénès | |
| 2016-11-11 | Coqide: fixing default local links for refman and stdlib. | Hugo Herbelin | |
| 2016-11-11 | Making explicit that a result is discarded (ocaml warning). | Hugo Herbelin | |
| 2016-11-10 | Remove unused feedback_content: Goals | CJ Bell | |
| 2016-11-10 | Move OSX script. | Maxime Dénès | |
| 2016-11-10 | Add Michael Soegtrop's new script to build windows installer. | Maxime Dénès | |
| 2016-11-10 | Remove old windows build scripts. | Maxime Dénès | |
| 2016-11-10 | Update CHANGES and credits for 8.6beta1. | Maxime Dénès | |
| 2016-11-10 | Updating a comment in test-suite. | Hugo Herbelin | |
| 2016-11-08 | Introducing a new EConstr.t type to perform the nf_evar operation on demand. | Pierre-Marie Pédrot | |
| 2016-11-08 | Merge commit 'b385fbb' into v8.6 | Maxime Dénès | |
| Was PR#347: Fix performance problem in pose proof | |||
| 2016-11-08 | Use pf_get_type_of to avoid blowup in pose proof of large proof terms | Matthieu Sozeau | |
| 2016-11-08 | Merge remote-tracking branch 'github/pr/348' into v8.6 | Maxime Dénès | |
| Was PR#348: Credits for 8.6 | |||
| 2016-11-08 | Update documentation of Arguments after recent changes. | Maxime Dénès | |
| 2016-11-08 | Rewording from Enrico | Matthieu Sozeau | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |