| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
This is only a quick fix, as hinted by Jason.
|
| |\
| |
| |
| | |
Was PR#366: Univs: fix bug 5208
|
| |\ \
| | |
| | |
| | | |
Was PR#378: Univs: fix bug #5188
|
| | | |
| | |
| | |
| | |
| | | |
Parameter was implemented the wrong way trying to separate the universes
of the telescope.
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
In the kernel's generic conversion, backtrack on UniverseInconsistency
for the unfolding heuristic (single backtracking point in reduction).
This exception can be raised in the univ_compare structure to produce
better error messages when the generic conversion function is called
from higher level code in reductionops.ml, which itself is called during
unification in evarconv.ml.
Inside the kernel, the infer and check variants of conversion never
raise UniverseInconsistency though, so this does not change the behavior
of the kernel.
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Universes are kept in normal form w.r.t. equality but not the <=
relation, so the previous check worked almost always but was actually
too strict! In cases like (max(Set,u) = u) when u is declared >= Set it
was failing to find an equality. Applying the KISS principle:
u = v <-> u <= v /\ v <= u.
Fix invariant breakage that triggered the discovery of the check_eq bug as well. No algebraic universes should appear in a term position (on the left of
a colon in a typing judgment), this was not the case when an algebraic
universe instantiated an evar that appeared in the term. We force their
universe variable status to change in refresh_universes to avoid this.
Fix ind sort inference: Use syntactic universe equality for inductive
sort inference instead of check_leq (which now correctly takes
constraints into account) and simplify code
|
| |\
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
- One was expecting shelved goals to remain after resolution (from refine).
- The other too were relying on the wrong classification of subgoals
as typeclass subgoals at toplevel.
|
| | | | | |
|
| | | | | |
|
| |\ \ \ \
| |_|/ /
|/| | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
Type annotations in unrelated binders were badly interfering with
detection of recursive binders in notations.
|
| |\| | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Refine fix for bug #4763, fixing #5149
Tactic [Refine.solve_constraints] and global option
Adds a new multi-goal tactic [Refine.solve_constraints] that forces solving of
unification constraints and evar candidates to be solved. run_tactic now calls
[solve_constraints] at every [.], preserving (mostly) the 8.4/8.5 behavior of tactics.
The option allows to unset the forced solving unification constraints at
each ".", letting the user control the places where the use of
heuristics is done.
Fix test-suite files too.
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Adds a compatibility flag so that the behavior of 8.5 can be obtained too.
Original commit:
unification.ml: fix for bug #4763, unif regression
Do not force all remaining conversions problems to be solved after
the _first_ solution of an evar. This was hell to track down, thanks
for the help of Maxime. contribs pass and HoTT too.
|
| | | | |
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This reverts commit 0b417c12eb10bb29bcee04384b6c0855cb9de73a.
A good fix requires to review a bit the design of unification constraint
postponement, which we do in 8.6. We leave things as they are in 8.5 for
compatibility.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
If an existing evar was cleared in pretyping (typically while
processing "ltac:"), it created an evar considered as new. Updating
them instead along the "cleared" flag.
If correct, I suspect similar treatment should be done for refining
along "change", "rename" and "move".
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The new algorithm produces different sets of arcs than in 8.5, hence
existing developments may fail to pass now because they relied on
the (correct but more approximate) result of minimization in 8.5 which
wasn't insensitive.
The algorithm works bottom-up on the (well-founded) graph to
find lower levels that an upper level can be minimized to. We
filter said lower levels according to the lower sets of the other levels
we consider. If they appear in any of them then we don't need their
constraints. Does not seem to have a huge impact on performance in HoTT,
but this should be evaluated further.
Adapt test-suite files accordingly.
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The commit which caused the regression (5ea2539d4a) looks reasonable.
However, it happens that this commit made that unification started in
the #4955 example to follow a path with problems of the form
"proj ?x == ?x" which clearly are unsolvable (both ?x have the same
instance).
We hack the corresponding very permissive occur-check function so that
it is a bit less permissive.
One day, this occur-check function would have to be rewritten in a
more stricter way.
----------------------------------------------------------------------
Extra comments:
I could list several functions for occur check of evars.
Four of them are too strict in the sense that they do not take into
account occurrences of evars which may disappear by reduction, nor
evars which have instances made in such a way that the occur-check is
solvable (as in "fst ?x[y:=(0,0)] = ?x[y:=0]"). These are:
- Termops.occur_evar for clenv, evar_refiner, tactic unification
- syntactic check without any normalization, even on defined evars
- Evarutil.occur_evar_upto for refine and the V82 compatibility mode
- syntactic check without any normalization but inlining of defined evars
- Evarsolve.occur_evar_upto_types for evar_define
- syntactic check without any normalization but inlining of defined evars
- occur-check in the type of evars met
- optimization for not visiting several time the same evar
- Evarsolve.noccur_evar for pattern unification and for inversion of
substitution (evar/evar or evar/term problems)
- syntactic check without any normalization but inlining of defined evars
- occur-check in the type of evars met in arguments of projections
- occur-check in the type of variables met in arguments of projections
- optimization for not visiting several time the same evar
- optimization for not visiting several time the type of the same variable
- note: to go this way, it seems to me that it should check also in
all types which are a cut-formula in the expression
One is much too lax:
- Evarconv.occur_rigidly
- no recursive check except on the types of "forall" and sometimes
in the arguments of an application
- note: there is obviously a large room for refinements without
loosing solutions
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
The fix solves the original bug report but it only turns the Not_found
into a normal error in the alternative example by Guillaume. See
test-suite file for comments on how to eventually improve the
situation and find a solution in Guillaume's example too.
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
When printing evar constraints, we ensure that every variable from the
rel context has a name.
|
| |\ \ \ \
| | |/ /
| |/| | |
|
| |\ \ \ \ |
|
| | |/| | | |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Previously, some splipped through and were caught by unrelated calls to
typeclass resolution.
|
| | |/ / /
| | | |
| | | |
| | | |
| | | | |
side_effects. Partial solution to the handling of side effects
in proofview.
|
| | | | | |
|
| |\| | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We simply catch the RetypeError raised by the retyping function and translate
it into a user error, so that it is captured by the tactic monad instead of
reaching toplevel.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
Evarconv was made precociously dependent on user-declared reduction
behaviors. Only cbn should rely on that.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Do not force all remaining conversions problems to be solved after the
_first_ solution of an evar, but only at the end of assignment of terms
to evars in w_merge. This was hell to track down, thanks for the help of
Maxime. contribs pass and HoTT too.
|
| |\| | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The patch is quite dumb: it essentially consists in alpha-renaming bound
module names when printing a functor, by checking that the name was not
already present, and generating a fresh one otherwise.
|
Hugo Herbelin
Maxime Dénès
Matthieu Sozeau
Jason Gross
Pierre-Marie Pédrot
Matthieu Sozeau