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/classfun.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/classfun.v')
| -rw-r--r-- | mathcomp/character/classfun.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v index 2cf17aa..468aa66 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.v @@ -1066,7 +1066,7 @@ have [-> | nzV] := eqVneq V 0; first by rewrite cfdot0r !mul0r subrr. by rewrite divfK ?cfnorm_eq0 ?subrr. Qed. -Lemma map_orthogonal M (nu : 'CF(G) -> 'CF(M)) S R (A : pred 'CF(G)) : +Lemma map_orthogonal M (nu : 'CF(G) -> 'CF(M)) S R (A : {pred 'CF(G)}) : {in A &, isometry nu} -> {subset S <= A} -> {subset R <= A} -> orthogonal (map nu S) (map nu R) = orthogonal S R. Proof. @@ -1290,7 +1290,7 @@ Section BuildIsometries. Variable (gT : finGroupType) (L G : {group gT}). Implicit Types (phi psi xi : 'CF(L)) (R S : seq 'CF(L)). -Implicit Types (U : pred 'CF(L)) (W : pred 'CF(G)). +Implicit Types (U : {pred 'CF(L)}) (W : {pred 'CF(G)}). Lemma sub_iso_to U1 U2 W1 W2 tau : {subset U2 <= U1} -> {subset W1 <= W2} -> |