aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/solvable/nilpotent.v
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp/solvable/nilpotent.v')
-rw-r--r--mathcomp/solvable/nilpotent.v7
1 files changed, 3 insertions, 4 deletions
diff --git a/mathcomp/solvable/nilpotent.v b/mathcomp/solvable/nilpotent.v
index 387ce34..d631919 100644
--- a/mathcomp/solvable/nilpotent.v
+++ b/mathcomp/solvable/nilpotent.v
@@ -75,10 +75,9 @@ Definition solvable :=
End PropertiesDefs.
-Arguments nilpotent _ _%g.
-Arguments nil_class _ _%g.
-Arguments solvable _ _%g.
-Prenex Implicits nil_class nilpotent solvable.
+Arguments nilpotent {_} _%g.
+Arguments nil_class {_} _%g.
+Arguments solvable {_} _%g.
Section NilpotentProps.