add declare scopes

6 files changed, 17 insertions, 1 deletions

diff --git a/mathcomp/algebra/Make b/mathcomp/algebra/Make
index dd1acef..8d89b59 100644
--- a/mathcomp/algebra/Make
+++ b/mathcomp/algebra/Make
@@ -25,4 +25,4 @@ zmodp.v
 -arg -w -arg -notation-overridden
 -arg -w -arg -duplicate-clear
 -arg -w -arg -ambiguous-paths
--arg -w -arg -undeclared-scope
\ No newline at end of file
+-arg -w -arg +undeclared-scope
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index 7899a62..cc3c6c6 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -135,6 +135,8 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Declare Scope matrix_set_scope.
+
 Import GroupScope.
 Import GRing.Theory.
 Local Open Scope ring_scope.
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index e9e9c45..e3de209 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -100,6 +100,8 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Declare Scope unity_root_scope.
+
 Import GRing.Theory.
 Local Open Scope ring_scope.
 
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index b449d66..455a79e 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -585,6 +585,10 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Declare Scope ring_scope.
+Declare Scope term_scope.
+Declare Scope linear_ring_scope.
+
 Reserved Notation "+%R" (at level 0).
 Reserved Notation "-%R" (at level 0).
 Reserved Notation "*%R" (at level 0, format " *%R").
diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v
index ca5a5e8..aa899b2 100644
--- a/mathcomp/algebra/ssrint.v
+++ b/mathcomp/algebra/ssrint.v
@@ -40,6 +40,10 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Declare Scope int_scope.
+Declare Scope distn_scope.
+Declare Scope rat_scope.
+
 Reserved Notation "n %:Z" (at level 2, left associativity, format "n %:Z").
 Reserved Notation "n = m :> 'in' 't'"
   (at level 70, m at next level, format "n  =  m  :>  'in' 't'").
diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v
index 462f8ad..e02aaef 100644
--- a/mathcomp/algebra/vector.v
+++ b/mathcomp/algebra/vector.v
@@ -91,6 +91,10 @@ From mathcomp Require Import ssralg matrix mxalgebra zmodp.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
+
+Declare Scope vspace_scope.
+Declare Scope lfun_scope.
+
 Local Open Scope ring_scope.
 
 Reserved Notation "{ 'vspace' T }" (at level 0, format "{ 'vspace'  T }").