| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| |\ \ |
|
| | | | |
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | | |
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.
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
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.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
| |
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
|
| |\ \ |
|
| | | |
| | |
| | |
| | | |
+ a few improvements on 5f1dd4c40 (lexing of { and }).
|
| | | | |
|
| | |/
|/|
| |
| |
| |
| |
| |
| | |
due to cleared/reverted section variables.
This fixes the get_type_of but requires keeping information
around about the section hyps available in goals during resolution.
It's optimized for the non-section case (should incur no cost there),
and the case where no section variables are cleared.
|
| |\ \ |
|
| | | |
| | |
| | |
| | | |
branches (see PR #323).
|
| |\ \ \
| | |/
| |/| |
|
| | | |
| | |
| | |
| | |
| | | |
This happens when recursive notations are used to define recursive
notations.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The move to systematically trying small inversion first bumps
sometimes as feared to the weakness of unification (see #5107).
----
Revert "Posssible abstractions over goal variables when inferring match return clause."
This reverts commit 0658ba7b908dad946200f872f44260d0e4893a94.
Revert "Trying an abstracting dependencies heuristic for the match return clause even when no type constraint is given."
This reverts commit 292f365185b7acdee79f3ff7b158551c2764c548.
Revert "Trying a no-inversion no-dependency heuristic for match return clause."
This reverts commit 2422aeb2b59229891508f35890653a9737988c00.
|
| | | | |
|
| | | |
| | |
| | |
| | | |
between proofs in tactic injection, with a side-effect on inversion.
|
| | | | |
|
| | |/
|/|
| |
| |
| |
| |
| | |
Since edb55a94fc5c0473e57f5a61c0c723194c2ff414 landed, compat notations
no longer modify the parser in non-compat-mode, so we can do this
without breaking Ltac parsing. Also update the related test-suite
files.
|
| | | |
|
| | | |
|
| |\ \
| | |
| | |
| | | |
Was PR#232: Fix the parsing of goal selectors.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The no-inversion and maximal abstraction over dependencies now
supports abstraction over goal variables rather than only on "rel"
variables. In particular, it now works consistently using
"intro H; refine (match H with ... end)" or
"refine (fun H => match H with ... end)".
By doing so, we ensure that all three strategies are tried in all
situations where a return clause has to be inferred, even in the
context of a "refine".
See antepenultimate commit for discussion.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
even when no type constraint is given.
This no-inversion and maximal abstraction over dependencies in (rel)
variables heuristic was used only when a type constraint was given.
By doing so, we ensure that all three strategies "inversion with
dependencies as evars", "no-inversion and maximal abstraction over
dependencies in (rel) variables", "no-inversion and no abstraction
over dependencies" are tried in all situations where a return clause
has to be inferred.
See penultimate commit for discussion.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The no-inversion no-dependency heuristic was used only in the absence
of type constraint. We may now use it also in the presence of a type
constraint.
See previous commit for discussion.
|
| | | | |
|
| | | | |
|
| |\ \ \
| | |/
| |/| |
|
| | | | |
|
| |\| | |
|
| | | | |
|
Maxime Dénès
Gaetan Gilbert
Tej Chajed
Guillaume Melquiond
Pierre-Marie Pédrot
Enrico Tassi
Ralf Jung
Théo Zimmermann
Hugo Herbelin
Matthieu Sozeau
Yves Bertot
Jason Gross