From c5763504783b51bb5def88c82f55a0b99ebf9d67 Mon Sep 17 00:00:00 2001 From: Georges Gonthier Date: Mon, 4 Mar 2019 11:49:56 +0100 Subject: 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. --- mathcomp/character/integral_char.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'mathcomp/character') diff --git a/mathcomp/character/integral_char.v b/mathcomp/character/integral_char.v index 3c2b0d6..d73f938 100644 --- a/mathcomp/character/integral_char.v +++ b/mathcomp/character/integral_char.v @@ -423,7 +423,7 @@ Theorem dvd_irr1_index_center gT (G : {group gT}) i : ('chi[G]_i 1%g %| #|G : 'Z('chi_i)%CF|)%C. Proof. without loss fful: gT G i / cfaithful 'chi_i. - rewrite -{2}[i](quo_IirrK _ (subxx _)) ?mod_IirrE ?cfModE ?cfker_normal //. + rewrite -{2}[i](quo_IirrK _ (subxx _)) 1?mod_IirrE ?cfModE ?cfker_normal //. rewrite morph1; set i1 := quo_Iirr _ i => /(_ _ _ i1) IH. have fful_i1: cfaithful 'chi_i1. by rewrite quo_IirrE ?cfker_normal ?cfaithful_quo. -- cgit v1.2.3