| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
|
|
variables
|
|
One didn't normalize the bodies of fixpoints according to the universe
context, resulting in a type errors. Use EConstr.to_constr to ensure
universes are normalized instead of using EConstr.Unsafe.to_constr.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
then only parsing
|
|
|
|
Notations were not initially designed to support independent parsing
and printing rules. Some redesign of this part of the code shall be
necessary at some time.
|
|
Earlier, the nat_syntax_plugin was loaded as soon as Datatypes.v.
This would now implies to make Datatypes.v depends on Decimal.v.
Instead, we postpone the Numeral Notation for nat until Prelude.v,
and we adapt those three tests that happen to live strictly between
Datatypes and Prelude.
|
|
(NB: only variables whose binder is inside the constructor argument,
ie
Inductive foo := C : forall A : Type -> Type, A Type -> foo.
does not trigger the bug because A becomes a RelKey.)
|
