| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
They were defined at level 70, no associativity in all but three places,
where they were instead declared at level 35.
Fixes #11890
|
|
Fixes #11846: Funind fails to generate principles for terms with let bindings.
|
|
Reviewed-by: SkySkimmer
|
|
|
|
A constraint can be stuck if it does not match any of the declared modes
for its head (if there are any). In that case, the subgoal is postponed
and the next ones are tried. We do a fixed point computation until there
are no stuck subgoals or the set does not change (it is impossible to
make it grow, as asserted in the code, because it is always a subset of
the initial goals)
This allows constraints on classes with modes to be treated as if they were
in any order (yay for stability of solutions!). Also, ultimately it should
free us to launch resolutions more agressively (avoiding issues like the
ones seen in PR #10762).
Add more examples of the semantics of TC resolution with apply in test-suite
Properly catch ModeMatchFailure on calls to map_e*
Add fixed bug 9058 to the test-suite
Close #9058
Add documentation
Fixes after Gaëtan's review.
Main change is to not use exceptions for control-flow
Update tactics/class_tactics.ml
Clearer and more efficient mode mismatch dispatch
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Remove exninfo argument
|
|
Reviewed-by: ppedrot
|
|
|
|
|
|
Reviewed-by: ppedrot
|
|
|
|
|
|
Fixes #11608.
This means -vos doesn't skip proofs for definitions that end with Qed
but don't include Proof and rely on a Set Default Proof Using. However,
this fixes the bug where this pattern would instead hang, due to #11564.
|
|
We avoid redundant notations for the same concepts and make sure
notations do not break Ltac parsing for users of these libraries.
|
|
Reviewed-by: tchajed
|
|
(inconsistencies in parsing/printing notations to partial applications)
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: jfehrle
|
|
Fix #11552: Ltac2 breaks query commands during proofs.
|
|
|
|
pattern-matching problem
Reviewed-by: ejgallego
|
|
In particular, this fixes #9741.
|
|
This was due to an inconsistency in handling implicit arguments in
the fields and in the constructor of a record.
|
|
|
|
We use the same kind of trick as the one we used for &IDENT, namely check
that no space appear between the dollar sign and the identifier.
|
|
Actually, callers of the Pvernac.register_proof_mode function have to
manually register the parsing of vernacular queries themselves. This
probably qualifies as an oversight from myself.
|
|
This fixes also #9640 part 1.
|
|
There was a collision at the time of interpreting subentries (in
metasyntax.ml) but also at the time of "optimizing" the entries (in
egramcoq.ml).
Also fixes #9517, fixes #9519, fixes #9640 (part 3).
|
|
of made up constant
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
|
|
There was an evar leak due to an evarmap not being threaded correctly
when computing open terms.
|
|
Fixes #5617.
|
|
|
|
Ack-by: Zimmi48
Reviewed-by: herbelin
Ack-by: maximedenes
|
|
Reviewed-by: ppedrot
|
|
Fixed by 8750682e367d7e78634bf88e667e4c9e7c3613d3 (#9915)
|
|
Seems to have been fixed since it was reported (perhaps by #11317?)
|
|
|
|
We typecheck arguments like previously, using bidirectionality hints,
but ultimately replace them with user-provided arguments on which we
replay coercion traces.
This is a fix which should be easy to backport, but there are two
directions of future work:
- Coercion traces for `Program` coercions (in these cases, we currently
use the inferred arguments)
- Separate the Coercion API in two phases: inference and application of
coercions. It will make the approach taken here cleaner, and probably
make it easier to interleave typing steps with coercion inference.
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
|
|
|
|
Check that we don't regress on PR #10762 example
Fix regression discovered by Arthur in PR #10762
Fix script of #10298 which was relying on breaking semantics for `eapply`
Add doc
Add comment in clenvtac
Actually, always mark shelved goals as unresolvable
Update doc to reflect semantics w.r.t. shelved subgoals
|
|
- Warn in some places where {x:T} is not assumed to occur (e.g. in
argument of an application, or of a match).
- Warn when an implicit argument occurs several times with the same name.
- Accept local anonymous {_:T} with explicitation possible using name `arg_k`.
We obtain this by using a flag (impl_binder_index) which tells if we
are in a position where implicit arguments matter and, if yes, the
index of the next binder.
|
|
library
Reviewed-by: ejgallego
|
|
universes
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: ppedrot
|
|
Using the parameter universes in the constructor causes implicit
equality constraints, so those universes may not be template
polymorphic.
A couple types in the stdlib were erroneously marked template, which
is now detected. Removing the marking doesn't actually change
behaviour though.
Also fixes #10504.
|
|
|
|
This is better than expecting other tests to fail if we mess up again.
|
