diff options
34 files changed, 82 insertions, 11 deletions
diff --git a/mathcomp/Make b/mathcomp/Make index 828a9e8..3cb12dd 100644 --- a/mathcomp/Make +++ b/mathcomp/Make @@ -99,3 +99,4 @@ ssreflect/tuple.v -arg -w -arg -duplicate-clear -arg -w -arg -ambiguous-paths -arg -w -arg +non-primitive-record +-arg -w -arg +undeclared-scope diff --git a/mathcomp/_CoqProject b/mathcomp/_CoqProject index 3b204ba..c2aa374 100644 --- a/mathcomp/_CoqProject +++ b/mathcomp/_CoqProject @@ -6,3 +6,4 @@ -arg -w -arg -notation-overridden -arg -w -arg -duplicate-clear -arg -w -arg +non-primitive-record +-arg -w -arg +undeclared-scope 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 }"). diff --git a/mathcomp/character/Make b/mathcomp/character/Make index deccc50..43790cd 100644 --- a/mathcomp/character/Make +++ b/mathcomp/character/Make @@ -14,4 +14,4 @@ vcharacter.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/character/classfun.v b/mathcomp/character/classfun.v index 356ff5c..ccfc37b 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.v @@ -91,6 +91,8 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Declare Scope cfun_scope. + Import Order.TTheory GroupScope GRing.Theory Num.Theory. Local Open Scope ring_scope. Delimit Scope cfun_scope with CF. diff --git a/mathcomp/character/mxabelem.v b/mathcomp/character/mxabelem.v index 949ded3..8575d58 100644 --- a/mathcomp/character/mxabelem.v +++ b/mathcomp/character/mxabelem.v @@ -47,6 +47,8 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Declare Scope abelem_scope. + Import GroupScope GRing.Theory FinRing.Theory. Local Open Scope ring_scope. diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v index e94e69f..6885ec7 100644 --- a/mathcomp/character/mxrepresentation.v +++ b/mathcomp/character/mxrepresentation.v @@ -282,6 +282,9 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Declare Scope irrType_scope. +Declare Scope group_ring_scope. + Import GroupScope GRing.Theory. Local Open Scope ring_scope. diff --git a/mathcomp/field/Make b/mathcomp/field/Make index cc0cd90..c906bd9 100644 --- a/mathcomp/field/Make +++ b/mathcomp/field/Make @@ -17,4 +17,4 @@ separable.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
\ No newline at end of file diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v index cd0a886..815bfba 100644 --- a/mathcomp/field/algC.v +++ b/mathcomp/field/algC.v @@ -53,6 +53,10 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Declare Scope C_scope. +Declare Scope C_core_scope. +Declare Scope C_expanded_scope. + Import Order.TTheory GRing.Theory Num.Theory. Local Open Scope ring_scope. diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v index 821a21e..bed8e71 100644 --- a/mathcomp/field/algnum.v +++ b/mathcomp/field/algnum.v @@ -41,6 +41,9 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Declare Scope algC_scope. +Declare Scope algC_expanded_scope. + Import GRing.Theory Num.Theory. Local Open Scope ring_scope. diff --git a/mathcomp/field/falgebra.v b/mathcomp/field/falgebra.v index db235fe..9069818 100644 --- a/mathcomp/field/falgebra.v +++ b/mathcomp/field/falgebra.v @@ -77,6 +77,10 @@ From mathcomp Require Import finalg zmodp matrix vector poly. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. + +Declare Scope aspace_scope. +Declare Scope lrfun_scope. + Local Open Scope ring_scope. Reserved Notation "{ 'aspace' T }" (at level 0, format "{ 'aspace' T }"). diff --git a/mathcomp/fingroup/Make b/mathcomp/fingroup/Make index 7f6b822..a765cd3 100644 --- a/mathcomp/fingroup/Make +++ b/mathcomp/fingroup/Make @@ -15,4 +15,4 @@ quotient.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
\ No newline at end of file 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. diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v index 38b3490..21e1e49 100644 --- a/mathcomp/fingroup/fingroup.v +++ b/mathcomp/fingroup/fingroup.v @@ -143,6 +143,9 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Declare Scope group_scope. +Declare Scope Group_scope. + Delimit Scope group_scope with g. Delimit Scope Group_scope with G. diff --git a/mathcomp/fingroup/presentation.v b/mathcomp/fingroup/presentation.v index af453aa..0137377 100644 --- a/mathcomp/fingroup/presentation.v +++ b/mathcomp/fingroup/presentation.v @@ -52,6 +52,9 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Declare Scope group_presentation. +Declare Scope nt_group_presentation. + Import GroupScope. Module Presentation. diff --git a/mathcomp/solvable/Make b/mathcomp/solvable/Make index 6101659..fd00057 100644 --- a/mathcomp/solvable/Make +++ b/mathcomp/solvable/Make @@ -26,4 +26,4 @@ sylow.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
\ No newline at end of file diff --git a/mathcomp/solvable/gfunctor.v b/mathcomp/solvable/gfunctor.v index 3417d84..2fcb8ac 100644 --- a/mathcomp/solvable/gfunctor.v +++ b/mathcomp/solvable/gfunctor.v @@ -81,12 +81,14 @@ From mathcomp Require Import quotient gproduct. (* structures when F1 is monotonic or hereditary, respectively. *) (******************************************************************************) -Import GroupScope. - Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Declare Scope gFun_scope. + +Import GroupScope. + Delimit Scope gFun_scope with gF. Module GFunctor. 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. diff --git a/mathcomp/solvable/jordanholder.v b/mathcomp/solvable/jordanholder.v index cd121cb..075c209 100644 --- a/mathcomp/solvable/jordanholder.v +++ b/mathcomp/solvable/jordanholder.v @@ -49,13 +49,14 @@ From mathcomp Require Import automorphism quotient action gseries. (* by Assia Mahboubi. *) (******************************************************************************) - -Import GroupScope. - Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Declare Scope section_scope. + +Import GroupScope. + Inductive section (gT : finGroupType) := GSection of {group gT} * {group gT}. Delimit Scope section_scope with sec. 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. |