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/character/character.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'mathcomp/character/character.v')

diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v
index e522924..6752623 100644
--- a/mathcomp/character/character.v
+++ b/mathcomp/character/character.v
@@ -390,8 +390,8 @@ Qed.
 
 End StandardRepresentation.
 
-Arguments grepr0 [R gT G].
-Prenex Implicits grepr0 dadd_grepr.
+Arguments grepr0 {R gT G}.
+Prenex Implicits dadd_grepr.
 
 Section Char.
 
@@ -924,7 +924,7 @@ Canonical char_semiringPred := SemiringPred mul_char.
 
 End IsChar.
 Prenex Implicits character.
-Arguments char_reprP [gT G phi].
+Arguments char_reprP {gT G phi}.
 
 Section AutChar.
 
@@ -2554,7 +2554,7 @@ Qed.
 
 End DerivedGroup.
 
-Arguments irr_prime_injP [gT G i].
+Arguments irr_prime_injP {gT G i}.
 
 (* Determinant characters and determinential order. *)
 Section DetOrder.
-- 
cgit v1.2.3