| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This allows to factorize code and prevents the unnecessary use of back and
forth conversions between the various types of terms.
Note that functions from typing may now raise errors as PretypeError rather
than TypeError, because they call the proper wrapper. I think that they were
wrongly calling the kernel because of an overlook of open modules.
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | | |
This also fixes decide equality, discriminate, ... (see e.g. #5279).
|
| | |\ \ \
| | | | |
| | | | |
| | | | | |
Was PR#172: alternate path separators in typeclass debug output.
|
| | |\ \ \ \
| | | |/ /
| | |/| | |
|
| | | |\ \ \
| | | | | |
| | | | | |
| | | | | | |
Was PR#381: V8.6+fix typeclasses eauto shelving
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
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.
|
| | | |/ / / |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This is while waiting for a deeper uniformization of auto, eauto, and
typeclasses eauto.
Incidentally includes a little fix in harmonizing auto/eauto printing.
|
| |/| | | |
| |/ / / |
|
| | | | |
| | | |
| | | |
| | | | |
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
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | | |
... in pose proof of large proof terms
|
| | | | | | | |
|
| | |\ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
Was PR#335: Fix printing of typeclasses eauto debug wrt intro.
|
| | |\ \ \ \ \ \
| | | | | | | |
| | | | | | | |
| | | | | | | | |
Was PR#336: Remove v62
|
| | | | | | | | | |
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
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.
|
| | | | | | | | | |
|
| | | | | | | | | |
|
Pierre-Marie Pédrot
Enrico Tassi
Hugo Herbelin
Maxime Dénès
Théo Zimmermann
Matthieu Sozeau