From bc0a71056c24b29c8289395ee01740bb2ef7ad8d Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 18 Nov 2019 17:40:51 +0100
Subject: [test suite] infrastructure to test how some statements are printed

---
 mathcomp/test_suite/output.v          |  4 +++
 mathcomp/test_suite/output.v.out      | 48 ++++++++++++++++++++++++++++++++++
 mathcomp/test_suite/output.v.out.8.12 | 48 ++++++++++++++++++++++++++++++++++
 mathcomp/test_suite/output.v.out.8.13 | 49 +++++++++++++++++++++++++++++++++++
 4 files changed, 149 insertions(+)
 create mode 100644 mathcomp/test_suite/output.v
 create mode 100644 mathcomp/test_suite/output.v.out
 create mode 100644 mathcomp/test_suite/output.v.out.8.12
 create mode 100644 mathcomp/test_suite/output.v.out.8.13

(limited to 'mathcomp/test_suite')

diff --git a/mathcomp/test_suite/output.v b/mathcomp/test_suite/output.v
new file mode 100644
index 0000000..706f15d
--- /dev/null
+++ b/mathcomp/test_suite/output.v
@@ -0,0 +1,4 @@
+From mathcomp Require Import all.
+
+Open Scope group_scope.
+About cyclic_pgroup_Aut_structure.
\ No newline at end of file
diff --git a/mathcomp/test_suite/output.v.out b/mathcomp/test_suite/output.v.out
new file mode 100644
index 0000000..bc5d3c8
--- /dev/null
+++ b/mathcomp/test_suite/output.v.out
@@ -0,0 +1,48 @@
+cyclic_pgroup_Aut_structure :
+forall [gT : finGroupType] [p : nat] [G : {group gT}],
+p.-group G ->
+cyclic G ->
+G != 1 :> {set gT} ->
+let q := #|G| in
+let n := (logn p q).-1 in
+let A := Aut G in
+let P := 'O_p(A) in
+let F := 'O_p^'(A) in
+exists m : {perm gT} -> 'Z_q,
+  [/\ [/\ {in A & G, forall (a : {perm gT}) (x : gT), x ^+ m a = a x},
+          m 1 = 1%R /\ {in A &, {morph m : a b / a * b >-> (a * b)%R}},
+          {in A &, injective m} /\ [seq m x | x in A] =i GRing.unit,
+          forall k : nat, {in A, {morph m : a / a ^+ k >-> (a ^+ k)%R}}
+        & {in A, {morph m : a / a^-1 >-> (a^-1)%R}}],
+      [/\ abelian A, cyclic F, #|F| = p.-1
+        & [faithful F, on 'Ohm_1(G) | [Aut G]]]
+    & if n == 0
+      then A = F
+      else
+       exists t : perm_for_finType gT,
+         [/\ t \in A, #[t] = 2, m t = (-1)%R
+           & if odd p
+             then
+              [/\ cyclic A /\ cyclic P,
+                  exists s : perm_for_finType gT,
+                    [/\ s \in A, #[s] = (p ^ n)%N, m s = (p.+1%:R)%R
+                      & P = <[s]>]
+                & exists s0 : perm_for_finType gT,
+                    [/\ s0 \in A, #[s0] = p, m s0 = ((p ^ n).+1%:R)%R
+                      & 'Ohm_1(P) = <[s0]>]]
+             else
+              if n == 1
+              then A = <[t]>
+              else
+               exists s : perm_for_finType gT,
+                 [/\ s \in A, #[s] = (2 ^ n.-1)%N, 
+                    m s = (5%:R)%R, <[s]> \x <[t]> = A
+                   & exists s0 : perm_for_finType gT,
+                       [/\ s0 \in A, #[s0] = 2, m s0 = ((2 ^ n).+1%:R)%R,
+                           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
+cyclic_pgroup_Aut_structure is opaque
+Expands to: Constant mathcomp.solvable.extremal.cyclic_pgroup_Aut_structure
diff --git a/mathcomp/test_suite/output.v.out.8.12 b/mathcomp/test_suite/output.v.out.8.12
new file mode 100644
index 0000000..bc5d3c8
--- /dev/null
+++ b/mathcomp/test_suite/output.v.out.8.12
@@ -0,0 +1,48 @@
+cyclic_pgroup_Aut_structure :
+forall [gT : finGroupType] [p : nat] [G : {group gT}],
+p.-group G ->
+cyclic G ->
+G != 1 :> {set gT} ->
+let q := #|G| in
+let n := (logn p q).-1 in
+let A := Aut G in
+let P := 'O_p(A) in
+let F := 'O_p^'(A) in
+exists m : {perm gT} -> 'Z_q,
+  [/\ [/\ {in A & G, forall (a : {perm gT}) (x : gT), x ^+ m a = a x},
+          m 1 = 1%R /\ {in A &, {morph m : a b / a * b >-> (a * b)%R}},
+          {in A &, injective m} /\ [seq m x | x in A] =i GRing.unit,
+          forall k : nat, {in A, {morph m : a / a ^+ k >-> (a ^+ k)%R}}
+        & {in A, {morph m : a / a^-1 >-> (a^-1)%R}}],
+      [/\ abelian A, cyclic F, #|F| = p.-1
+        & [faithful F, on 'Ohm_1(G) | [Aut G]]]
+    & if n == 0
+      then A = F
+      else
+       exists t : perm_for_finType gT,
+         [/\ t \in A, #[t] = 2, m t = (-1)%R
+           & if odd p
+             then
+              [/\ cyclic A /\ cyclic P,
+                  exists s : perm_for_finType gT,
+                    [/\ s \in A, #[s] = (p ^ n)%N, m s = (p.+1%:R)%R
+                      & P = <[s]>]
+                & exists s0 : perm_for_finType gT,
+                    [/\ s0 \in A, #[s0] = p, m s0 = ((p ^ n).+1%:R)%R
+                      & 'Ohm_1(P) = <[s0]>]]
+             else
+              if n == 1
+              then A = <[t]>
+              else
+               exists s : perm_for_finType gT,
+                 [/\ s \in A, #[s] = (2 ^ n.-1)%N, 
+                    m s = (5%:R)%R, <[s]> \x <[t]> = A
+                   & exists s0 : perm_for_finType gT,
+                       [/\ s0 \in A, #[s0] = 2, m s0 = ((2 ^ n).+1%:R)%R,
+                           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
+cyclic_pgroup_Aut_structure is opaque
+Expands to: Constant mathcomp.solvable.extremal.cyclic_pgroup_Aut_structure
diff --git a/mathcomp/test_suite/output.v.out.8.13 b/mathcomp/test_suite/output.v.out.8.13
new file mode 100644
index 0000000..0546b70
--- /dev/null
+++ b/mathcomp/test_suite/output.v.out.8.13
@@ -0,0 +1,49 @@
+cyclic_pgroup_Aut_structure :
+forall [gT : finGroupType] [p : nat] [G : {group gT}],
+p.-group G ->
+cyclic G ->
+G != 1 :> {set gT} ->
+let q := #|G| in
+let n := (logn p q).-1 in
+let A := Aut G in
+let P := 'O_p(A) in
+let F := 'O_p^'(A) in
+exists m : {perm gT} -> 'Z_q,
+  [/\ [/\ {in A & G, forall (a : {perm gT}) (x : gT), x ^+ m a = a x},
+          m 1 = 1%R /\ {in A &, {morph m : a b / a * b >-> (a * b)%R}},
+          {in A &, injective m} /\ [seq m x | x in A] =i GRing.unit,
+          forall k : nat, {in A, {morph m : a / a ^+ k >-> (a ^+ k)%R}}
+        & {in A, {morph m : a / a^-1 >-> (a^-1)%R}}],
+      [/\ abelian A, cyclic F, #|F| = p.-1
+        & [faithful F, on 'Ohm_1(G) | [Aut G]]]
+    & if n == 0
+      then A = F
+      else
+       exists t : perm_for_finType gT,
+         [/\ t \in A, #[t] = 2, m t = (-1)%R
+           & if odd p
+             then
+              [/\ cyclic A /\ cyclic P,
+                  exists s : perm_for_finType gT,
+                    [/\ s \in A, #[s] = (p ^ n)%N, m s = (p.+1%:R)%R
+                      & P = <[s]>]
+                & exists s0 : perm_for_finType gT,
+                    [/\ s0 \in A, #[s0] = p, m s0 = ((p ^ n).+1%:R)%R
+                      & 'Ohm_1(P) = <[s0]>]]
+             else
+              if n == 1
+              then A = <[t]>
+              else
+               exists s : perm_for_finType gT,
+                 [/\ s \in A, #[s] = (2 ^ n.-1)%N, 
+                    m s = (5%:R)%R, <[s]> \x <[t]> = A
+                   & exists s0 : perm_for_finType gT,
+                       [/\ s0 \in A, #[s0] = 2, m s0 = ((2 ^ n).+1%:R)%R,
+                           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 _ _
+  _
+cyclic_pgroup_Aut_structure is opaque
+Expands to: Constant mathcomp.solvable.extremal.cyclic_pgroup_Aut_structure
-- 
cgit v1.2.3


From c0214cdb4a44261db539b48fb76dbdaded87312b Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 9 Sep 2020 15:22:29 +0200
Subject: default reference file for < 8.12

---
 mathcomp/test_suite/output.v.out | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'mathcomp/test_suite')

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
-- 
cgit v1.2.3


From c7b1927d8072040d573757d543e2355e8280b9ee Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 10 Sep 2020 15:22:50 +0200
Subject: new attempt

---
 mathcomp/test_suite/output.v          |  2 +-
 mathcomp/test_suite/output.v.out      | 91 +++++++++++++++++------------------
 mathcomp/test_suite/output.v.out.8.12 | 48 ------------------
 mathcomp/test_suite/output.v.out.8.13 | 49 -------------------
 4 files changed, 45 insertions(+), 145 deletions(-)
 delete mode 100644 mathcomp/test_suite/output.v.out.8.12
 delete mode 100644 mathcomp/test_suite/output.v.out.8.13

(limited to 'mathcomp/test_suite')

diff --git a/mathcomp/test_suite/output.v b/mathcomp/test_suite/output.v
index 706f15d..7e9def3 100644
--- a/mathcomp/test_suite/output.v
+++ b/mathcomp/test_suite/output.v
@@ -1,4 +1,4 @@
 From mathcomp Require Import all.
 
 Open Scope group_scope.
-About cyclic_pgroup_Aut_structure.
\ No newline at end of file
+Check @cyclic_pgroup_Aut_structure.
\ No newline at end of file
diff --git a/mathcomp/test_suite/output.v.out b/mathcomp/test_suite/output.v.out
index 122ddf0..4db5888 100644
--- a/mathcomp/test_suite/output.v.out
+++ b/mathcomp/test_suite/output.v.out
@@ -1,48 +1,45 @@
-cyclic_pgroup_Aut_structure :
-forall (gT : finGroupType) (p : nat) (G : {group gT}),
-p.-group G ->
-cyclic G ->
-G != 1 :> {set gT} ->
-let q := #|G| in
-let n := (logn p q).-1 in
-let A := Aut G in
-let P := 'O_p(A) in
-let F := 'O_p^'(A) in
-exists m : {perm gT} -> 'Z_q,
-  [/\ [/\ {in A & G, forall (a : {perm gT}) (x : gT), x ^+ m a = a x},
-          m 1 = 1%R /\ {in A &, {morph m : a b / a * b >-> (a * b)%R}},
-          {in A &, injective m} /\ [seq m x | x in A] =i GRing.unit,
-          forall k : nat, {in A, {morph m : a / a ^+ k >-> (a ^+ k)%R}}
-        & {in A, {morph m : a / a^-1 >-> (a^-1)%R}}],
-      [/\ abelian A, cyclic F, #|F| = p.-1
-        & [faithful F, on 'Ohm_1(G) | [Aut G]]]
-    & if n == 0
-      then A = F
-      else
-       exists t : perm_for_finType gT,
-         [/\ t \in A, #[t] = 2, m t = (-1)%R
-           & if odd p
-             then
-              [/\ cyclic A /\ cyclic P,
-                  exists s : perm_for_finType gT,
-                    [/\ s \in A, #[s] = (p ^ n)%N, m s = (p.+1%:R)%R
-                      & P = <[s]>]
-                & exists s0 : perm_for_finType gT,
-                    [/\ s0 \in A, #[s0] = p, m s0 = ((p ^ n).+1%:R)%R
-                      & 'Ohm_1(P) = <[s0]>]]
+cyclic_pgroup_Aut_structure
+     : forall (gT : finGroupType) (p : nat) (G : {group gT}),
+       p.-group G ->
+       cyclic G ->
+       G != 1 ->
+       let q := #|G| in
+       let n := (logn p q).-1 in
+       let A := Aut G in
+       let P := 'O_p(A) in
+       let F := 'O_p^'(A) in
+       exists m : {perm gT} -> 'Z_q,
+         [/\ [/\ {in A & G, forall (a : {perm gT}) (x : gT), x ^+ m a = a x},
+                 m 1 = 1%R /\ {in A &, {morph m : a b / a * b >-> (a * b)%R}},
+                 {in A &, injective m} /\ [seq m x | x in A] =i GRing.unit,
+                 forall k : nat,
+                 {in A, {morph m : a / a ^+ k >-> (a ^+ k)%R}}
+               & {in A, {morph m : a / a^-1 >-> (a^-1)%R}}],
+             [/\ abelian A, cyclic F, #|F| = p.-1
+               & [faithful F, on 'Ohm_1(G) | [Aut G]]]
+           & if n == 0
+             then A = F
              else
-              if n == 1
-              then A = <[t]>
-              else
-               exists s : perm_for_finType gT,
-                 [/\ s \in A, #[s] = (2 ^ n.-1)%N, 
-                    m s = (5%:R)%R, <[s]> \x <[t]> = A
-                   & exists s0 : perm_for_finType gT,
-                       [/\ s0 \in A, #[s0] = 2, m s0 = ((2 ^ n).+1%:R)%R,
-                           m (s0 * t) = ((2 ^ n).-1%:R)%R
-                         & 'Ohm_1(<[s]>) = <[s0]>]]]]
-
-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
+              exists t : perm_for_finType gT,
+                [/\ t \in A, #[t] = 2, m t = (-1)%R
+                  & if odd p
+                    then
+                     [/\ cyclic A /\ cyclic P,
+                         exists s : perm_for_finType gT,
+                           [/\ s \in A, #[s] = (p ^ n)%N, m s = (p.+1%:R)%R
+                             & P = <[s]>]
+                       & exists s0 : perm_for_finType gT,
+                           [/\ s0 \in A, #[s0] = p, m s0 = ((p ^ n).+1%:R)%R
+                             & 'Ohm_1(P) = <[s0]>]]
+                    else
+                     if n == 1
+                     then A = <[t]>
+                     else
+                      exists s : perm_for_finType gT,
+                        [/\ s \in A, #[s] = (2 ^ n.-1)%N, 
+                           m s = (5%:R)%R, <[s]> \x <[t]> = A
+                          & exists s0 : perm_for_finType gT,
+                              [/\ s0 \in A, #[s0] = 2,
+                                  m s0 = ((2 ^ n).+1%:R)%R,
+                                  m (s0 * t) = ((2 ^ n).-1%:R)%R
+                                & 'Ohm_1(<[s]>) = <[s0]>]]]]
diff --git a/mathcomp/test_suite/output.v.out.8.12 b/mathcomp/test_suite/output.v.out.8.12
deleted file mode 100644
index bc5d3c8..0000000
--- a/mathcomp/test_suite/output.v.out.8.12
+++ /dev/null
@@ -1,48 +0,0 @@
-cyclic_pgroup_Aut_structure :
-forall [gT : finGroupType] [p : nat] [G : {group gT}],
-p.-group G ->
-cyclic G ->
-G != 1 :> {set gT} ->
-let q := #|G| in
-let n := (logn p q).-1 in
-let A := Aut G in
-let P := 'O_p(A) in
-let F := 'O_p^'(A) in
-exists m : {perm gT} -> 'Z_q,
-  [/\ [/\ {in A & G, forall (a : {perm gT}) (x : gT), x ^+ m a = a x},
-          m 1 = 1%R /\ {in A &, {morph m : a b / a * b >-> (a * b)%R}},
-          {in A &, injective m} /\ [seq m x | x in A] =i GRing.unit,
-          forall k : nat, {in A, {morph m : a / a ^+ k >-> (a ^+ k)%R}}
-        & {in A, {morph m : a / a^-1 >-> (a^-1)%R}}],
-      [/\ abelian A, cyclic F, #|F| = p.-1
-        & [faithful F, on 'Ohm_1(G) | [Aut G]]]
-    & if n == 0
-      then A = F
-      else
-       exists t : perm_for_finType gT,
-         [/\ t \in A, #[t] = 2, m t = (-1)%R
-           & if odd p
-             then
-              [/\ cyclic A /\ cyclic P,
-                  exists s : perm_for_finType gT,
-                    [/\ s \in A, #[s] = (p ^ n)%N, m s = (p.+1%:R)%R
-                      & P = <[s]>]
-                & exists s0 : perm_for_finType gT,
-                    [/\ s0 \in A, #[s0] = p, m s0 = ((p ^ n).+1%:R)%R
-                      & 'Ohm_1(P) = <[s0]>]]
-             else
-              if n == 1
-              then A = <[t]>
-              else
-               exists s : perm_for_finType gT,
-                 [/\ s \in A, #[s] = (2 ^ n.-1)%N, 
-                    m s = (5%:R)%R, <[s]> \x <[t]> = A
-                   & exists s0 : perm_for_finType gT,
-                       [/\ s0 \in A, #[s0] = 2, m s0 = ((2 ^ n).+1%:R)%R,
-                           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
-cyclic_pgroup_Aut_structure is opaque
-Expands to: Constant mathcomp.solvable.extremal.cyclic_pgroup_Aut_structure
diff --git a/mathcomp/test_suite/output.v.out.8.13 b/mathcomp/test_suite/output.v.out.8.13
deleted file mode 100644
index 0546b70..0000000
--- a/mathcomp/test_suite/output.v.out.8.13
+++ /dev/null
@@ -1,49 +0,0 @@
-cyclic_pgroup_Aut_structure :
-forall [gT : finGroupType] [p : nat] [G : {group gT}],
-p.-group G ->
-cyclic G ->
-G != 1 :> {set gT} ->
-let q := #|G| in
-let n := (logn p q).-1 in
-let A := Aut G in
-let P := 'O_p(A) in
-let F := 'O_p^'(A) in
-exists m : {perm gT} -> 'Z_q,
-  [/\ [/\ {in A & G, forall (a : {perm gT}) (x : gT), x ^+ m a = a x},
-          m 1 = 1%R /\ {in A &, {morph m : a b / a * b >-> (a * b)%R}},
-          {in A &, injective m} /\ [seq m x | x in A] =i GRing.unit,
-          forall k : nat, {in A, {morph m : a / a ^+ k >-> (a ^+ k)%R}}
-        & {in A, {morph m : a / a^-1 >-> (a^-1)%R}}],
-      [/\ abelian A, cyclic F, #|F| = p.-1
-        & [faithful F, on 'Ohm_1(G) | [Aut G]]]
-    & if n == 0
-      then A = F
-      else
-       exists t : perm_for_finType gT,
-         [/\ t \in A, #[t] = 2, m t = (-1)%R
-           & if odd p
-             then
-              [/\ cyclic A /\ cyclic P,
-                  exists s : perm_for_finType gT,
-                    [/\ s \in A, #[s] = (p ^ n)%N, m s = (p.+1%:R)%R
-                      & P = <[s]>]
-                & exists s0 : perm_for_finType gT,
-                    [/\ s0 \in A, #[s0] = p, m s0 = ((p ^ n).+1%:R)%R
-                      & 'Ohm_1(P) = <[s0]>]]
-             else
-              if n == 1
-              then A = <[t]>
-              else
-               exists s : perm_for_finType gT,
-                 [/\ s \in A, #[s] = (2 ^ n.-1)%N, 
-                    m s = (5%:R)%R, <[s]> \x <[t]> = A
-                   & exists s0 : perm_for_finType gT,
-                       [/\ s0 \in A, #[s0] = 2, m s0 = ((2 ^ n).+1%:R)%R,
-                           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 _ _
-  _
-cyclic_pgroup_Aut_structure is opaque
-Expands to: Constant mathcomp.solvable.extremal.cyclic_pgroup_Aut_structure
-- 
cgit v1.2.3


From f3ad9538962cd36d90ea3a6724125f448d7c0b10 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 11 Sep 2020 09:52:42 +0200
Subject: fix 8.9, 8.8 and 8.7

---
 mathcomp/test_suite/output.v.out.8.7 |  1 +
 mathcomp/test_suite/output.v.out.8.8 |  1 +
 mathcomp/test_suite/output.v.out.8.9 | 46 ++++++++++++++++++++++++++++++++++++
 3 files changed, 48 insertions(+)
 create mode 120000 mathcomp/test_suite/output.v.out.8.7
 create mode 120000 mathcomp/test_suite/output.v.out.8.8
 create mode 100644 mathcomp/test_suite/output.v.out.8.9

(limited to 'mathcomp/test_suite')

diff --git a/mathcomp/test_suite/output.v.out.8.7 b/mathcomp/test_suite/output.v.out.8.7
new file mode 120000
index 0000000..896b7ac
--- /dev/null
+++ b/mathcomp/test_suite/output.v.out.8.7
@@ -0,0 +1 @@
+output.v.out.8.9
\ No newline at end of file
diff --git a/mathcomp/test_suite/output.v.out.8.8 b/mathcomp/test_suite/output.v.out.8.8
new file mode 120000
index 0000000..896b7ac
--- /dev/null
+++ b/mathcomp/test_suite/output.v.out.8.8
@@ -0,0 +1 @@
+output.v.out.8.9
\ No newline at end of file
diff --git a/mathcomp/test_suite/output.v.out.8.9 b/mathcomp/test_suite/output.v.out.8.9
new file mode 100644
index 0000000..25583d5
--- /dev/null
+++ b/mathcomp/test_suite/output.v.out.8.9
@@ -0,0 +1,46 @@
+cyclic_pgroup_Aut_structure
+     : forall (gT : finGroupType) (p : nat) (G : {group gT}),
+       p.-group G ->
+       cyclic G ->
+       G != 1 ->
+       let q := #|G| in
+       let n := (logn p q).-1 in
+       let A := Aut G in
+       let P := 'O_p(A) in
+       let F := 'O_p^'(A) in
+       exists m : {perm gT} -> 'Z_q,
+         [/\ [/\ {in A & G, forall (a : {perm gT}) (x : gT), x ^+ m a = a x},
+                 m 1 = 1%R /\ {in A &, {morph m : a b / a * b >-> (a * b)%R}},
+                 {in A &, injective m} /\ [seq m x | x in A] =i GRing.unit,
+                 forall k : nat,
+                 {in A, {morph m : a / a ^+ k >-> 
+                 (a ^+ k)%R}}
+               & {in A, {morph m : a / a^-1 >-> (a^-1)%R}}],
+             [/\ abelian A, cyclic F, #|F| = p.-1
+               & [faithful F, on 'Ohm_1(G) | [Aut G]]]
+           & if n == 0
+             then A = F
+             else
+              exists t : perm_for_finType gT,
+                [/\ t \in A, #[t] = 2, m t = (-1)%R
+                  & if odd p
+                    then
+                     [/\ cyclic A /\ cyclic P,
+                         exists s : perm_for_finType gT,
+                           [/\ s \in A, #[s] = (p ^ n)%N, m s = (p.+1%:R)%R
+                             & P = <[s]>]
+                       & exists s0 : perm_for_finType gT,
+                           [/\ s0 \in A, #[s0] = p, m s0 = ((p ^ n).+1%:R)%R
+                             & 'Ohm_1(P) = <[s0]>]]
+                    else
+                     if n == 1
+                     then A = <[t]>
+                     else
+                      exists s : perm_for_finType gT,
+                        [/\ s \in A, #[s] = (2 ^ n.-1)%N, 
+                           m s = (5%:R)%R, <[s]> \x <[t]> = A
+                          & exists s0 : perm_for_finType gT,
+                              [/\ s0 \in A, #[s0] = 2,
+                                  m s0 = ((2 ^ n).+1%:R)%R,
+                                  m (s0 * t) = ((2 ^ n).-1%:R)%R
+                                & 'Ohm_1(<[s]>) = <[s0]>]]]]
-- 
cgit v1.2.3


From 38b28c7d9756da7d346a1866a4ce712b1c3472af Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 14 Sep 2020 15:11:14 +0200
Subject: don't use all.v in output.v

---
 mathcomp/test_suite/output.v | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'mathcomp/test_suite')

diff --git a/mathcomp/test_suite/output.v b/mathcomp/test_suite/output.v
index 7e9def3..b0b0996 100644
--- a/mathcomp/test_suite/output.v
+++ b/mathcomp/test_suite/output.v
@@ -1,4 +1,10 @@
-From mathcomp Require Import all.
+From mathcomp Require Import
+  all_ssreflect
+  all_algebra
+  all_field
+  all_character
+  all_fingroup
+  all_solvable.
 
 Open Scope group_scope.
 Check @cyclic_pgroup_Aut_structure.
\ No newline at end of file
-- 
cgit v1.2.3