| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |\
| |
| |
| | |
Was needed to be done for a while.
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| | |
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 was not working when the inductive type had implicit parameters.
This could still be improved. E.g. the following still does not work:
Reserved Notation "#".
Inductive I {A:Type} := C : # where "#" := I.
But it should be made working by taking care of adding the mandatory
implicit argument A at the time # is interpreted as [@I _]
(i.e., technically speaking, using expl_impls in interp_notation).
|
| | | | | |
|
| | |/ /
|/| | |
|
| | | | |
|
| |\ \ \
| | |/
| |/| |
|
| | | |
| | |
| | |
| | |
| | | |
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.
|
| | | | |
|
| |\ \ \
| | | |
| | | |
| | | | |
Was PR#366: Univs: fix bug 5208
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
Was PR#378: Univs: fix bug #5188
|
| | | | | | |
|
| |\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
Was PR#377: Univs: fix bug #5180
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
Parameter was implemented the wrong way trying to separate the universes
of the telescope.
|
| | |/ / / /
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
| |/ / / /
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| | | | | | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
Now [typeclasses eauto] mimicks what happens during resolution
faithfully, and the shelving behavior/requirements for a successful
proof-search are documented.
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
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.
|
| |\ \ \ \ \ \
| |_|/ / / /
|/| | | / /
| | |_|/ /
| |/| | | |
|
| |\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
Was PR#321: Handling of section variables in hints
|
| |\ \ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
Was PR#319: More error tagging, try to fix bug 5135
|
Hugo Herbelin
Maxime Dénès
Gaetan Gilbert
Tej Chajed
Ralf Jung
Pierre-Marie Pédrot
Matthieu Sozeau
Théo Zimmermann
Jason Gross