| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | | | | | | |
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
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.
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
"Hint Resolve <->" now behaves the same as "Hint Resolve", in that it uses
the same default locality and it accepts locality prefixes.
|
| | | | | | | | |
|
| | | |_|_|_|/
| |/| | | | |
|
| | | |/ / /
| |/| | | |
|
| | | |/ /
| |/| | |
|
| | | |/
| |/| |
|
| | | | |
|
| | | |
| | |
| | |
| | | |
#3339).
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
This is while waiting for a deeper uniformization of auto, eauto, and
typeclasses eauto.
Incidentally includes a little fix in harmonizing auto/eauto printing.
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | | |
| | |
| | |
| | | |
This reverts commit 81c9fa0de99400b51c029cdbd1519b4f724e320a.
|
| | |/ |
|
| | | |
|
| | |\
| | |
| | |
| | | |
Was PR#360: [stm] Remove STM-related vernaculars
|
| | |\ \
| | | |
| | | |
| | | | |
Was PR#192: Add test suite files for 4700-4785
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| | |\ \ \
| | | | |
| | | | |
| | | | | |
Was PR#362: Revert another part of a477dc in good measure
|
| | | | | |
| | | | |
| | | | |
| | | | | |
Hit by OCaml's "if then else" with no "end" once more
|
| | | | |/
| | |/|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| | |\ \ \
| | |/ /
| |/| |
| | | | |
Was PR#361: [doc] Mention XML protocol on changes.
|
| | |/ /
| | |
| | |
| | | |
It may be worth it, also added a note about file reorganization.
|
| | |\ \
| | | |
| | | |
| | | | |
Was PR#358: Revert part of a477dc, disallow_shelved
|
| | |/ /
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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
|
| | | |
| | |
| | |
| | |
| | | |
The recommended way to install Coq under windows is anyway to use the
precompiled installer.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | | |
We could not produce an exhaustive list of such fixes, and the
usefulness of such a list is not clear.
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | |\ \
| | | |
| | | |
| | | | |
Was PR#347: Fix performance problem in pose proof
|
| | | | | |
|
| | |\ \ \
| | | | |
| | | | |
| | | | | |
Was PR#348: Credits for 8.6
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | |\ \ \ \
| | |_|/ /
| |/| | |
| | | | | |
Was PR#339: Documenting type class options, typeclasses eauto
|
| | | | | | |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
They allow to call refine without doing typeclass resolution, allowing
to use refine in typeclass hints.
|
| | | | | | |
|
Guillaume Melquiond
Jason Gross
Hugo Herbelin
Pierre-Marie Pédrot
Maxime Dénès
Théo Zimmermann
Enrico Tassi
Jason Gross
Emilio Jesus Gallego Arias
Matthieu Sozeau