diff options
| author | Enrico Tassi | 2020-09-09 15:22:29 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2020-09-09 15:22:29 +0200 |
| commit | c0214cdb4a44261db539b48fb76dbdaded87312b (patch) | |
| tree | fdd46aacafb2b4a685193283841ef95a6df9786b /mathcomp/test_suite | |
| parent | bc0a71056c24b29c8289395ee01740bb2ef7ad8d (diff) | |
default reference file for < 8.12
Diffstat (limited to 'mathcomp/test_suite')
| -rw-r--r-- | mathcomp/test_suite/output.v.out | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mathcomp/test_suite/output.v.out b/mathcomp/test_suite/output.v.out index bc5d3c8..122ddf0 100644 --- a/mathcomp/test_suite/output.v.out +++ b/mathcomp/test_suite/output.v.out @@ -1,5 +1,5 @@ cyclic_pgroup_Aut_structure : -forall [gT : finGroupType] [p : nat] [G : {group gT}], +forall (gT : finGroupType) (p : nat) (G : {group gT}), p.-group G -> cyclic G -> G != 1 :> {set gT} -> @@ -42,7 +42,7 @@ exists m : {perm gT} -> 'Z_q, m (s0 * t) = ((2 ^ n).-1%:R)%R & 'Ohm_1(<[s]>) = <[s0]>]]]] -cyclic_pgroup_Aut_structure is not universe polymorphic -Arguments cyclic_pgroup_Aut_structure [gT] [p]%nat_scope [G]%Group_scope +Arguments gT, p, G are implicit +Argument scopes are [_ nat_scope Group_scope _ _ _] cyclic_pgroup_Aut_structure is opaque Expands to: Constant mathcomp.solvable.extremal.cyclic_pgroup_Aut_structure |