aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/solvable/gseries.v
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp/solvable/gseries.v')
-rw-r--r--mathcomp/solvable/gseries.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/mathcomp/solvable/gseries.v b/mathcomp/solvable/gseries.v
index 73188a6..43ed7db 100644
--- a/mathcomp/solvable/gseries.v
+++ b/mathcomp/solvable/gseries.v
@@ -32,6 +32,8 @@ Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
+Declare Scope group_rel_scope.
+
Import GroupScope.
Section GroupDefs.