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')

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