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/solvable | |
| 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/solvable')
| -rw-r--r-- | mathcomp/solvable/gfunctor.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/solvable/gfunctor.v b/mathcomp/solvable/gfunctor.v index 31ffded..3417d84 100644 --- a/mathcomp/solvable/gfunctor.v +++ b/mathcomp/solvable/gfunctor.v @@ -266,7 +266,7 @@ Variable F : GFunctor.iso_map. Lemma gFsub gT (G : {group gT}) : F gT G \subset G. Proof. by case: F gT G. Qed. -Lemma gFsub_trans gT (G : {group gT}) (A : pred_class) : +Lemma gFsub_trans gT (G : {group gT}) (A : {pred gT}) : G \subset A -> F gT G \subset A. Proof. exact/subset_trans/gFsub. Qed. @@ -297,7 +297,7 @@ Proof. exact/char_trans/gFchar. Qed. Lemma gFnormal_trans gT (G H : {group gT}) : H <| G -> F gT H <| G. Proof. exact/char_normal_trans/gFchar. Qed. -Lemma gFnorm_trans gT (A : pred_class) (G : {group gT}) : +Lemma gFnorm_trans gT (A : {pred gT}) (G : {group gT}) : A \subset 'N(G) -> A \subset 'N(F gT G). Proof. by move/subset_trans/(_ (gFnorms G)). Qed. |