diff options
| author | Georges Gonthier | 2019-04-29 17:59:14 +0200 |
|---|---|---|
| committer | GitHub | 2019-04-29 17:59:14 +0200 |
| commit | c3b8865dbf01c857b6b619c620095c0385f66977 (patch) | |
| tree | ee443d2cf69970aece83d93435fe598994fbf8ff /mathcomp/character/character.v | |
| parent | 8e27a1dd704c8f7a34de29d65337eb67254a1741 (diff) | |
| parent | dae54440f08364552e1a82ac7984f35d1864f1e5 (diff) | |
Merge pull request #337 from math-comp/coq-ssrbool-refactor-compat
Generalise use of `{pred T}` from coq/coq#9995
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. |