diff options
| author | Georges Gonthier | 2019-04-28 20:37:17 +0200 |
|---|---|---|
| committer | Georges Gonthier | 2019-04-29 00:26:36 +0200 |
| commit | 6be8fd5c67949a59bde7083e81401263986e7a4e (patch) | |
| tree | 71a6e45e4948db3a459906982a5b2b982470108c /mathcomp/character/character.v | |
| parent | 8e27a1dd704c8f7a34de29d65337eb67254a1741 (diff) | |
Generalise use of `{pred T}` from coq/coq#9995
Use `{pred T}` systematically for generic _collective_ boolean
predicate.
Use `PredType` to construct `predType` instances.
Instrument core `ssreflect` files to replicate these and other new
features introduces by coq/coq#9555 (`nonPropType` interface,
`simpl_rel` that simplifies with `inE`).
Diffstat (limited to 'mathcomp/character/character.v')
| -rw-r--r-- | mathcomp/character/character.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v index 862e1ba..c2a7ef4 100644 --- a/mathcomp/character/character.v +++ b/mathcomp/character/character.v @@ -572,10 +572,10 @@ Lemma irr_of_socleK : cancel irr_of_socle W. Proof. by move=> Wi; rewrite /W subrK cast_ordKV enum_rankK. Qed. Hint Resolve socle_of_IirrK irr_of_socleK : core. -Lemma irr_of_socle_bij (A : pred (Iirr G)) : {on A, bijective irr_of_socle}. +Lemma irr_of_socle_bij (A : {pred (Iirr G)}) : {on A, bijective irr_of_socle}. Proof. by apply: onW_bij; exists W. Qed. -Lemma socle_of_Iirr_bij (A : pred sG) : {on A, bijective W}. +Lemma socle_of_Iirr_bij (A : {pred sG}) : {on A, bijective W}. Proof. by apply: onW_bij; exists irr_of_socle. Qed. End IrrClassDef. |