| Age | Commit message (Collapse) | Author |
|---|
|
This introduces the warning “not-a-class” in the “typeclasses” category.
|
|
|
|
|
|
|
|
|
|
|
|
broken
|
|
|
|
This fixes #8791.
We explicitly specify for intro the names of binders which are
given by the user. This still can suffer from spurious collisions,
see #8819.
|
|
The compilation to bytecode of the elimination schemes for int31 must
happen after the int31 type is registered to the retroknowledge.
Otherwise, the “decompint” instruction is not emitted.
|
|
|
|
|
|
We compute the binding to tactic-in-term once for all in the right
scopes before interpreting the tactic.
An alternative would have been to surround the constr_expr by
CDelimiters to simulate its interpretation in the expected scopes
(though this would not have worked for temporary scopes).
|
|
|
|
|
|
Ltac_plugin.Taccoerce.CannotCoerceTo.
|
|
|
|
|
|
|
|
|
|
|
|
Lintian found some spelling errors in the Debian packaging for coq. Fix
them most places they appear in the current source. (Don't change
documentation anchor names, as that would invalidate external
deeplinks.)
This also fixes a bug in coqdoc: prior to this commit, coqdoc would
highlight `instanciate` but not `instantiate`.
|
|
|
|
|
|
|
|
Note that since this now reduces before restricting universes
behaviour may be a bit different.
|
|
See commit [Simplify code for [Definition := Eval ...]] which without
this breaks test suite 7631.v
|
|
|
|
They were allowed to stay in terms in some cases. We now ensure that if
an evar is defined as e.g. fun x => Type@{foo}, foo is properly
refreshed to be non-algebraic as it could otherwise appear in the term
and break the invariant.
Also cleanup the implementation of refresh_universes to avoid using a
mutable reference and simply rely on the Constr.map smartmap idiom
instead.
This might have compatibility issues, e.g. in HoTT where maybe more
non-algebraic proxy universes could be generated, we'll see.
For the bug report proper, there is a lack of bidirectional
type-checking that makes the initial definition fail (there's a
non-canonical choice of dependency if we don't consider the typing
constraint). With the Program bidir hint it passes.
|
|
|
|
|
|
|
|
|
|
|
|
Mostly via `dev/tools/update-compat.py --cur-version=8.9`
We just remove test-suite/success/FunindExtraction_compat86.v because,
except for the `Extraction iszero.` line at the bottom, it is a
duplicate of `test-suite/success/Funind.v` (except with `-compat 8.6`).
We also manually update a number of test-suite files to pre-emptively
remove compatibility notations (which used to be compat 8.6, but are now
compat 8.7).
|
|
All changes done with
```
git grep --name-only 'compat "8.6"' | xargs sed -i s'/compat "8.6"/compat "8.7"/g'
```
As per https://github.com/coq/coq/pull/8374#issuecomment-426202818 and
https://github.com/coq/coq/issues/8383#issuecomment-426200497
|
|
|
|
We raise a normal error instead of an anomaly.
|
|
We raise a normal error instead of an anomaly.
This fixes also #2550, #8492.
Note in passing: While the case of a type "Inductive I := list I -> I"
is difficult, the case of a "Inductive I := list nat -> I" should be
easily doable.
|
|
Instead of looking into the name-oriented structure we look into the
actual section structures.
Note: together with #8475 this lets us remove UnivNames.add_global_universe.
|
|
|
|
|
|
evars by name
|
|
The regression was introduced in 1522b989 (PR #7193) which itself was
fixing bug #7192. (Note another regression of the same commit which is
fixed in #8416.)
|
|
|
|
When interpreting an existential variable "?n@{inst}" in the current
context, check that variables bound to local definitions are replaced
by variables with convertible body.
Also give a message explaining the type error or non-convertibility
error rather than wrongly saying that there is no binding for the
variable.
|
|
|
|
|
|
|
|
This refines even further c24bcae8 (PR #924) and 6304c843:
- c24bcae8 fixed the order in the heuristic
- 6304c843 improved the order by preferring projections
There remained a dependency in the alphabetic order in selecting
unification candidates. The current commit fixes it.
We radically change the representation of the substitution to invert
by using a map indexed on the rank in the signature rather than on the
name of the variable.
More could be done to use numbers further, e.g. for representing
aliases.
Note that this has consequences on the test-suite (in
output/Notations.v) as some problems now infer a dependent return
clause.
|
