From f049e51c39077a025907ea87c08178dad1841801 Mon Sep 17 00:00:00 2001
From: Anton Trunov
Date: Tue, 20 Nov 2018 17:51:11 +0100
Subject: Merge Arguments and Prenex Implicits

See the discussion here:
https://github.com/math-comp/math-comp/pull/242#discussion_r233778114
---
 mathcomp/solvable/sylow.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'mathcomp/solvable/sylow.v')

diff --git a/mathcomp/solvable/sylow.v b/mathcomp/solvable/sylow.v
index dd45afa..f940ec9 100644
--- a/mathcomp/solvable/sylow.v
+++ b/mathcomp/solvable/sylow.v
@@ -535,8 +535,7 @@ Qed.
 
 End Zgroups.
 
-Arguments Zgroup _ _%g.
-Prenex Implicits Zgroup.
+Arguments Zgroup {_} _%g.
 
 Section NilPGroups.
 
-- 
cgit v1.2.3