| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | |\ \ \
| | | | |
| | | | |
| | | | | |
Was PR#172: alternate path separators in typeclass debug output.
|
| | |\ \ \ \
| | | |/ /
| | |/| | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Before this fix, unshelve typeclasses eauto would produce sub-goals
in the reverse order compared to when they were first shelved.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
| |/| | | |
| |/ / / |
|
| | | | |
| | | |
| | | |
| | | | |
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.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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
|
| | |\ \ \
| | | | |
| | | | |
| | | | | |
Was PR#339: Documenting type class options, typeclasses eauto
|
| | |\ \ \ \
| | | | | |
| | | | | |
| | | | | | |
Was PR#331: Solve_constraints and Set Use Unification Heuristics
|
| | |\ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
Was PR#335: Fix printing of typeclasses eauto debug wrt intro.
|
| | | | | | | | |
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
This commit makes the traversing strategy of typeclasses
eauto an optional argument of the function that implements
it.
This change should be non-breaking.
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
be the instance writer's responsibility to not generated non-dependent
non-class subgoals (otherwise we loose compatibility as shown in
e.g. MathClasses, which goes into loops because of unexpectedly
unconstrained goals). Reflect it in the doc.
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Now [typeclasses eauto] mimicks what happens during resolution
faithfully, and the shelving behavior/requirements for a successful
proof-search are documented.
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
This was the source of a bug in #5115#c7.
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | |_|/ / /
| |/| | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
In addition to a priority, cleanup the interfaces for passing this
information as well. The pattern, if given, takes priority over the
inferred one.
We only allow Existing Instances gr ... gr | pri. for now, without
pattern, as before.
Make the API compatible to 8.5 as well.
|
| |\| | | | | |
|
| | | | | | | |
|
| | | |/ / /
| | | | |
| | | | |
| | | | |
| | | | | |
reconsider_conv_pbs -> reconsider_unif_constraints
consider_remaining_unif_problems -> solve_unif_constraints_with_heuristics
|
| | |/ / /
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
due to cleared/reverted section variables.
This fixes the get_type_of but requires keeping information
around about the section hyps available in goals during resolution.
It's optimized for the non-section case (should incur no cost there),
and the case where no section variables are cleared.
|
| |\| | | |
|
| | | | | |
|
| | | |/
| |/|
| | |
| | | |
unresolvable
|
| |\| | |
|
Pierre-Marie Pédrot
Maxime Dénès
Théo Zimmermann
Matthieu Sozeau