aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/fingroup/action.v
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp/fingroup/action.v')
-rw-r--r--mathcomp/fingroup/action.v3
1 files changed, 3 insertions, 0 deletions
diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v
index 3679b75..dfcb5ac 100644
--- a/mathcomp/fingroup/action.v
+++ b/mathcomp/fingroup/action.v
@@ -122,6 +122,9 @@ Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
+Declare Scope action_scope.
+Declare Scope groupAction_scope.
+
Import GroupScope.
Section ActionDef.