diff options
| author | Georges Gonthier | 2019-03-04 11:49:56 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2019-04-01 17:42:37 +0200 |
| commit | c5763504783b51bb5def88c82f55a0b99ebf9d67 (patch) | |
| tree | 1c67f83da1617ba441027206ee03a9c1e2fc6e9f /plugin | |
| parent | 8a62590dd06803fca626f429271f9ad578f06a96 (diff) | |
Compatibility fix for Coq issue coq/#9663
Coq currently fails to resolve Miller patterns against open evars
(issue coq/#9663), in particular it fails to unify `T -> ?R` with
`forall x : T, ?dR x` even when `?dR` does not have `x` in its context.
As a result canonical structures and constructor notations for the
new generalised dependent `finfun`s fail for the non-dependent use
cases, which is an unacceptable regression.
This commit mitigates the problem by specialising the canonical
instances and most of the constructor notation to the non-dependent
case, and introducing an alias of the `finfun_of` type that has
canonical instances for the dependent case, to allow experimentation
with that feature.
With this fix the whole `MathComp` library compiles, with a few
minor changes. The change in `integral_char` fixes a performance issue
that appears to be the consequence of insufficient locking of both
`finfun_eqType` and `cfIirr`; this will be explored in a further commit.
Diffstat (limited to 'plugin')
0 files changed, 0 insertions, 0 deletions