| Age | Commit message (Collapse) | Author |
|---|
|
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
|
|
if the .vos file is empty, rename -quick to -vio, dump empty .vos when producing .vio, dump empty .vos and .vok files when producing .vo from .vio.
|
|
only-printing notations
Ack-by: cpitclaudel
Reviewed-by: ejgallego
|
|
containing letins.
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: ejgallego
|
|
|
|
This governs the printing of the explicitation of implicit arguments
and the removal of coercions.
E.g., "Check coe foo." where coe is a coercion with codomain B will show:
foo
: B
instead of
coe foo
: B
|
|
Fixes #10971
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
Failing on CProdN([],...) was maybe a bit too radical.
|
|
- 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.
|
|
We renounce to the ad hoc rule preferring a notation w/o delimiter
for a term with coercions stripped over a notation for the
fully-applied terms with coercions not removed.
Instead, we interleave removal of coercions and search for notations:
we prefer a notation for the fully applied term, and, if not, try to
remove one coercion, and try again a notation for the remaining term,
and if not, try to remove the next coercion, etc.
Note: the flatten_application could be removed if prim_token were able
to apply on a prefix of an application node.
|
|
Reviewed-by: JasonGross
Reviewed-by: ejgallego
Reviewed-by: maximedenes
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
|
|
The missing dependency impacted the algorithm for detecting default
clauses.
|
|
Reviewed-by: gares
Reviewed-by: herbelin
|
|
And simplify a lot the compatibility infrastructure following this.
Update dev/tools/update-compat.py
Remove much complexity.
Co-authored-by: Jason Gross <jgross@mit.edu>
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: silene
|
|
Reviewed-by: SkySkimmer
Reviewed-by: cpitclaudel
|
|
The manual was already saying that it was deprecated, but no warning was
emitted.
Fixes #10572
|
|
library
Reviewed-by: ejgallego
|
|
|
|
c.f. discussion at
https://github.com/coq/coq/pull/11177#issuecomment-559139477
|
|
In particular, display how long they took in bogomips-adjusted
centiseconds.
|
|
|
|
universes
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: ppedrot
|
|
Reviewed-by: herbelin
|
|
This increases backwards compatibility. If desired, we can add a tactic
notation to simplify the spec of `rapply` in the future if we want.
|
|
Also add a tactic notation so that it takes in uconstrs by default.
Also add some basic tests for `rapply`.
Also document rapply in the manual
|
|
Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com>
|
|
refined version of #8890 which prevents #11033.
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
|
|
Reviewed-by: ejgallego
|
|
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.
|
|
Reviewed-by: ejgallego
Reviewed-by: herbelin
|
|
|
|
This is to hopefully prevent regressions on
https://github.com/coq/coq/issues/11150 and
https://github.com/coq/coq/issues/6502.
|
|
This is better than expecting other tests to fail if we mess up again.
|
|
We restrict #8890 so that it looks for a notation only for the fully
applied coercion.
|
|
`Fixpoint` with a let binder
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
Reviewed-by: gares
Reviewed-by: silene
|
|
"similar" means sharing a scope or implicit status.
|
|
(fixing bug #11057).
With this new behavior, it is not needed to .vos files in user contribs.
Also, this commit adds a feature: upon creation of a .vo file, an empty .vok file is touched.
|
|
|
|
We can now do `#[refine] Instance : Bla := bli.` to enter proof mode
with `bli` as a starting refinement.
If `bli` is enough to define the instance we still enter proof mode,
keeping things nicely predictable for the stm.
|
|
Reviewed-by: ppedrot
|
|
Ack-by: Blaisorblade
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
This should ideally have been done before the 8.11 branching.
|
|
Reviewed-by: ppedrot
|
