| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
| |
We use heaps instead of continuously adding elements to an ordered list,
which was quadratic in the worst case.
As a byproduct, this solves bug #5359, which was due to a stack overflow on
big lists.
|
| |\ |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | | |
Bug #4957 was "unify cannot directly unify universes with evars, but can
do so indirectly".
|
| |\| | |
|
| | |\ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
Fixes Coq bug 5345 (https://coq.inria.fr/bugs/show_bug.cgi?id=5345):
Cannot use names bound in matches inside Ltac definitions.
|
| |\| | | |
|
| | |/ /
| | |
| | |
| | |
| | |
| | | |
Fixes [Coq bug #5372](https://coq.inria.fr/bugs/show_bug.cgi?id=5372)
"Anomaly: Not a valid information when defining mutual fixpoints that
are not mutual with Function".
|
| |\| | |
|
| | |\ \
| | | |
| | | |
| | | | |
correctly as…
|
| | |_|/
|/| |
| | |
| | |
| | | |
This commit removes from the source tree plugins/decl_mode,
its chapter in the reference manual and related tests.
|
| |\ \ \
| | | |
| | | |
| | | | |
Tactic Notation
|
| |\ \ \ \
| | |/ /
| |/| | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This is cumbersome, because now code may fail at link time if it's not
referring to the correct module name. Therefore, one has to add corresponding
open statements a the top of every file depending on a Ltac module. This
includes seemingly unrelated files that use EXTEND statements.
|
| | | | | |
|
| | |/ /
|/| |
| | |
| | | |
In particular, this closes bug 2417.
|
| |\| | |
|
| | |\ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
This was introduced in 8.5 while reorganizing the structure of
intro-patterns.
|
| | |\| | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Tracking conversion problems to reconsider was lost for evars subject
to restriction (field last_mods was not updated and conversion
problems not considered to be changed).
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
A cleaning done in ade2363e35 (Dec 2015) was hinting at bugs in typing
a matching over a "catch-all" variable, when let-ins occur in the
arity. However ade2363e35 failed to understand what was the correct
fix, introducing instead the regressions mentioned in #5322 and #5324.
This fixes all of #5322 and #5324, as well as the handling of let-ins
in the arity.
Thanks to Jason for helping in diagnosing the problem.
|
| |/ / /
| | |
| | |
| | | |
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.
|
| | | | | |
|
| |\| | | |
|
Pierre-Marie Pédrot
Maxime Dénès
Tej Chajed
Enrico Tassi
Hugo Herbelin
Théo Zimmermann
Matthieu Sozeau
Jason Gross
Matthieu Sozeau