From 2525c33691e25f837b7dca31d4c702199b3dbc5d Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Sun, 4 Mar 2018 16:57:06 -0800
Subject: Change deprecated Arguments Scope to Arguments

---
 mathcomp/fingroup/morphism.v | 21 ++++++++++-----------
 1 file changed, 10 insertions(+), 11 deletions(-)

(limited to 'mathcomp/fingroup/morphism.v')

diff --git a/mathcomp/fingroup/morphism.v b/mathcomp/fingroup/morphism.v
index 315358b..32c01d3 100644
--- a/mathcomp/fingroup/morphism.v
+++ b/mathcomp/fingroup/morphism.v
@@ -144,8 +144,8 @@ Definition ker mph := morphpre mph 1.
 
 End MorphismOps1.
 
-Arguments Scope morphim [_ _ group_scope _ _ group_scope].
-Arguments Scope morphpre [_ _ group_scope _ _ group_scope].
+Arguments morphim _ _ _%g _ _ _%g.
+Arguments morphpre _ _ _%g _ _ _%g.
 
 Notation "''dom' f" := (dom (MorPhantom f))
   (at level 10, f at level 8, format "''dom'  f") : group_scope.
@@ -908,7 +908,7 @@ Proof. exact: morphim_idm. Qed.
 
 End IdentityMorphism.
 
-Arguments Scope idm [_ group_scope group_scope].
+Arguments idm _ _%g _%g.
 Prenex Implicits idm.
 
 Section RestrictedMorphism.
@@ -967,7 +967,7 @@ Proof. by move <-; exists f. Qed.
 
 End RestrictedMorphism.
 
-Arguments Scope restrm [_ _ group_scope group_scope _ group_scope].
+Arguments restrm _ _ _%g _%g _ _%g.
 Prenex Implicits restrm.
 Arguments restrmP [aT rT A D].
 Arguments domP [aT rT A D].
@@ -994,8 +994,7 @@ Proof. by apply/setIidPl/subsetP=> x _; rewrite !inE /=. Qed.
 
 End TrivMorphism.
 
-Arguments Scope trivm [_ _ group_scope group_scope].
-Arguments trivm {aT rT}.
+Arguments trivm {aT rT} _%g _%g.
 
 (* The composition of two morphisms is a Canonical morphism instance. *)
 Section MorphismComposition.
@@ -1325,10 +1324,10 @@ Proof. exact: restr_isom_to. Qed.
 
 End ReflectProp.
 
-Arguments Scope isom [_ _ group_scope group_scope _].
-Arguments Scope morphic [_ _ group_scope _].
-Arguments Scope misom [_ _ group_scope group_scope _].
-Arguments Scope isog [_ _ group_scope group_scope].
+Arguments isom _ _ _%g _%g _.
+Arguments morphic _ _ _%g _.
+Arguments misom _ _ _%g _%g _.
+Arguments isog _ _ _%g _%g.
 
 Arguments morphicP [aT rT A f].
 Arguments misomP [aT rT A B f].
@@ -1479,7 +1478,7 @@ Qed.
 
 End Homg.
 
-Arguments Scope homg [_ _ group_scope group_scope].
+Arguments homg _ _ _%g _%g.
 Notation "G \homg H" := (homg G H)
   (at level 70, no associativity) : group_scope.
 
-- 
cgit v1.2.3