Merge pull request #656 from affeldt-aist/declare_scopes

add declare scopes

10 files changed, 22 insertions, 1 deletions

diff --git a/mathcomp/ssreflect/Make b/mathcomp/ssreflect/Make
index b5e2038..d6879a6 100644
--- a/mathcomp/ssreflect/Make
+++ b/mathcomp/ssreflect/Make
@@ -30,5 +30,5 @@ order.v
 -arg -w -arg -notation-overridden
 -arg -w -arg -duplicate-clear
 -arg -w -arg -ambiguous-paths
--arg -w -arg -undeclared-scope
+-arg -w -arg +undeclared-scope
 -arg -w -arg -non-reversible-notation
\ No newline at end of file
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index 0ece733..cd3507a 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -100,6 +100,8 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Declare Scope big_scope.
+
 Reserved Notation "\big [ op / idx ]_ i F"
   (at level 36, F at level 36, op, idx at level 10, i at level 0,
      right associativity,
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index 1225ad9..a844aa8 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -115,6 +115,9 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Declare Scope eq_scope.
+Declare Scope fun_delta_scope.
+
 Module Equality.
 
 Definition axiom T (e : rel T) := forall x y, reflect (x = y) (e x y).
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index 5b6e4d0..3e60c2d 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -110,6 +110,9 @@ From mathcomp Require Import choice fintype finfun bigop.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
+
+Declare Scope set_scope.
+
 Section SetType.
 
 Variable T : finType.
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index b125ba5..a8b677d 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -156,6 +156,8 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Declare Scope fin_quant_scope.
+
 Module Finite.
 
 Section RawMixin.
diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v
index c8b1490..726877c 100644
--- a/mathcomp/ssreflect/generic_quotient.v
+++ b/mathcomp/ssreflect/generic_quotient.v
@@ -88,6 +88,8 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Declare Scope quotient_scope.
+
 Reserved Notation "\pi_ Q" (at level 0, format "\pi_ Q").
 Reserved Notation "\pi" (at level 0, format "\pi").
 Reserved Notation "{pi_ Q a }"
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index 1546a55..7cd178d 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -407,6 +407,9 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Declare Scope order_scope.
+Declare Scope cpo_sort.
+
 Delimit Scope order_scope with O.
 Local Open Scope order_scope.
 
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 9747171..c658ac2 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -190,6 +190,8 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Declare Scope seq_scope.
+
 Reserved Notation "[ '<->' P0 ; P1 ; .. ; Pn ]"
   (at level 0, format "[ '<->' '['  P0 ;  '/' P1 ;  '/'  .. ;  '/'  Pn ']' ]").
 
diff --git a/mathcomp/ssreflect/ssrAC.v b/mathcomp/ssreflect/ssrAC.v
index 47b85e4..41c0109 100644
--- a/mathcomp/ssreflect/ssrAC.v
+++ b/mathcomp/ssreflect/ssrAC.v
@@ -56,6 +56,7 @@ Unset Printing Implicit Defensive.
 (* ...                                                                  *)
 (************************************************************************)
 
+Declare Scope AC_scope.
 
 Delimit Scope AC_scope with AC.
 
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index 0a2fbcd..dcb518f 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -106,6 +106,9 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Declare Scope coq_nat_scope.
+Declare Scope nat_rec_scope.
+
 (* Disable Coq prelude hints to improve proof script robustness. *)
 
 Remove Hints plus_n_O plus_n_Sm mult_n_O mult_n_Sm : core.