diff options
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/Make | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/poly.v | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/ssralg.v | 4 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrint.v | 4 | ||||
| -rw-r--r-- | mathcomp/algebra/vector.v | 4 |
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 }"). |
