| Age | Commit message (Collapse) | Author |
|---|
|
Try just going with the user-given names, and not worrying about
what happens with repeated names or anonymous implicits.
(Support for anonymous implicits is due to herbelin in #11098.)
This PR should not change behaviour in the absence of repeated names.
Since repeated names are already a poorly handled corner case, I would
recommend changing binder names to avoid overlap in the case of a
change in behavior.
Since anonymous implicits and implicits with repeated names can already
happen, I think this is unlikely to cause too many new problems,
though it might exacerbate existing ones. However, I already had to fix
one newly possible anomaly, so I can't be too confident.
The most common change in external developments was that an argument
no longer gets `0` appended to it, causing the `Arguments` command
to complain about renaming.
To fix this and keep the old name, one can simply use the `rename` flag
as suggested, or switch to the new, un-suffixed name.
Closes #6785
Closes #12001
Another step towards checking the standard library with `-mangle-names`.
|
|
Apparently the `Timeout` exception is raised by a signal handled, and
that can happen when the running thread is a worker manager, rather than
the main thread (the one that should be interrupted).
Given that the point of these tests is to test *auto and not the STM,
we disable async proofs forcibly.
|
|
A constraint can be stuck if it does not match any of the declared modes
for its head (if there are any). In that case, the subgoal is postponed
and the next ones are tried. We do a fixed point computation until there
are no stuck subgoals or the set does not change (it is impossible to
make it grow, as asserted in the code, because it is always a subset of
the initial goals)
This allows constraints on classes with modes to be treated as if they were
in any order (yay for stability of solutions!). Also, ultimately it should
free us to launch resolutions more agressively (avoiding issues like the
ones seen in PR #10762).
Add more examples of the semantics of TC resolution with apply in test-suite
Properly catch ModeMatchFailure on calls to map_e*
Add fixed bug 9058 to the test-suite
Close #9058
Add documentation
Fixes after Gaëtan's review.
Main change is to not use exceptions for control-flow
Update tactics/class_tactics.ml
Clearer and more efficient mode mismatch dispatch
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Remove exninfo argument
|
|
|
|
|
|
|
|
|
|
|
|
|
|
A file in the test-suite had to be modified.
It was supposed to reproduce a behavior in intuistionistic-nuprl
but it did not really.
This commit is not supposed to break intuistionistic-nuprl.
|
|
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.
|
|
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
|
|
Now [typeclasses eauto] mimicks what happens during resolution
faithfully, and the shelving behavior/requirements for a successful
proof-search are documented.
|
|
|
|
|
|
|
|
Fix test-suite files
|
|
Add an option to force backtracking at toplevel, which
is used by default when calling typeclasses eauto on a set of goals.
They might be depended on by other subgoals, so the tactic should
be backtracking by default, a once can make it not backtrack.
|
|
Fix typo in proofview
|
|
|
|
Obviously broken since r13359 (remove native Π)...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13502 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
typeclass resolution. Fixes a bug reported by Eelis van der Weegen.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12545 85f007b7-540e-0410-9357-904b9bb8a0f7
|
