| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| | |_|/
|/| | |
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Otherwise [(fun x => x) (Type : Type@{_})] becomes
[(fun x : Type@{i+1} => x) (Type@{i} : Type@{i+1})]
breaking the invariant that terms do not contain algebraic universes
(at the lambda abstraction).
|
| | | | |
| | | |
| | | |
| | | | |
The addition to the test suite showcases the usage.
|
| |\ \ \ \
| |/ / /
|/| | | |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
let-ins
|
| | |_|_|/
|/| | | |
|
| |\ \ \ \ |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
To use the generic combinator, we introduce a side effect. I believe
that we have more to gain from a short code than from being purely
functional.
This also fixes the expected semantics since the variables binding the
return type in "match" were not taking into account.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Binding generalizable_vars_of_glob_constr, occur_glob_constr,
free_glob_vars, and bound_glob_vars on it.
Most of the functions of which it factorizes the code were bugged with
respect to bindings in the return clause of "match" and in either the
types or the bodies of "fix/cofix".
|
| |\ \ \ \ \
| |_|_|_|/
|/| | | |
| | | | | |
record fields.
|
| | |_|_|/
|/| | |
| | | |
| | | | |
Also remove obvious comments.
|
| |\ \ \ \ |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | | |
This is a test for commit 9d1230d484a2cf519f9cd76dc0f37815f3c6339b.
|
| | | | | |
| | | | |
| | | | |
| | | | | |
in the presence of let-ins.
|
| |\ \ \ \ \
| | |_|_|/
| |/| | | |
|
| | |\ \ \ \ |
|
| | | | | | |\
| | | | | | |
| | | | | | |
| | | | | | | |
Was needed to be done for a while.
|
| | | |/ / / /
| |/| | | | |
|
| |\| | | | | |
|
| | |\ \ \ \ \
| | | |_|/ /
| | |/| | | |
|
| | | | | | | |
|
| |\| | | | | |
|
| | | |_|/ /
| |/| | | |
|
| | |\| | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Fixes Coq bug 5345 (https://coq.inria.fr/bugs/show_bug.cgi?id=5345):
Cannot use names bound in matches inside Ltac definitions.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
That way, (IZR 5) is no longer reduced to 2 + 1 + 1 + 1 (which is not
convertible to 5) but instead to 1 + 2 * 2 (which is). Moreover, it means
that, after reduction, real constants no longer exponentially blow up.
Note that I was not able to fix the test-suite for the declarative mode,
so the missing proof terms have been admitted.
|
| | |\| | | |
|
| | | |/ /
| |/| |
| | | |
| | | |
| | | | |
This commit removes from the source tree plugins/decl_mode,
its chapter in the reference manual and related tests.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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).
|
| | | | | |
|
| | | | | |
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Interpretation of patterns in Ltac is essentially flawed. It does a roundtrip
through the pretyper, and relies on suspicious flagging of evars in the evar source
field to recognize original pattern holes. After the pattern_of_constr function
was made evar-insensitive, it expanded evars that were solved by magical side-effects
of the pretyper, even if it hadn't been asked to perform any heuristics.
We backtrack on the insensitivity of the pattern_of_constr function. This may have
a performance penalty in other dubious code, e.g. hints. In the long run we should
get rid of the pattern_of_constr function.
|
| | |/ / /
| | | |
| | | |
| | | | |
In particular, this closes bug 2417.
|
| | |\| | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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 also fixes decide equality, discriminate, ... (see e.g. #5279).
|
| | |\ \
| | | |
| | | |
| | | | |
Was PR#366: Univs: fix bug 5208
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| | |/ /
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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
|
| | | |
| | |
| | |
| | |
| | |
| | | |
- 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.
|
Maxime Dénès
Hugo Herbelin
Gaetan Gilbert
Jason Gross
Pierre-Marie Pédrot
Tej Chajed
Guillaume Melquiond
Enrico Tassi
Ralf Jung
Théo Zimmermann
Matthieu Sozeau