Merge pull request #249 from anton-trunov/prenex-implicits

Merge Arguments and Prenex Implicits

1 files changed, 7 insertions, 8 deletions

diff --git a/mathcomp/solvable/cyclic.v b/mathcomp/solvable/cyclic.v
index bed8c5c..046f4a2 100644
--- a/mathcomp/solvable/cyclic.v
+++ b/mathcomp/solvable/cyclic.v
@@ -289,11 +289,11 @@ Proof. by rewrite /order => /(<[a]> =P _)->. Qed.
 
 End Cyclic.
 
-Arguments cyclic _ _%g.
-Arguments generator _ _%g _%g.
-Arguments expg_invn _ _%g _%N.
-Arguments cyclicP [gT A].
-Prenex Implicits cyclic Zpm generator expg_invn.
+Arguments cyclic {_} _%g.
+Arguments generator {_}_%g _%g.
+Arguments expg_invn {_} _%g _%N.
+Arguments cyclicP {gT A}.
+Prenex Implicits cyclic Zpm.
 
 (* Euler's theorem *)
 Theorem Euler_exp_totient a n : coprime a n -> a ^ totient n  = 1 %[mod n].
@@ -556,9 +556,8 @@ Qed.
 
 End Metacyclic.
 
-Arguments metacyclic _ _%g.
-Prenex Implicits metacyclic.
-Arguments metacyclicP [gT A].
+Arguments metacyclic {_} _%g.
+Arguments metacyclicP {gT A}.
 
 (* Automorphisms of cyclic groups. *)
 Section CyclicAutomorphism.