diff options
Diffstat (limited to 'mathcomp/algebra/fraction.v')
| -rw-r--r-- | mathcomp/algebra/fraction.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/algebra/fraction.v b/mathcomp/algebra/fraction.v index 8cf811a..98eb9f1 100644 --- a/mathcomp/algebra/fraction.v +++ b/mathcomp/algebra/fraction.v @@ -16,8 +16,8 @@ Unset Strict Implicit. Unset Printing Implicit Defensive. Import GRing.Theory. -Open Local Scope ring_scope. -Open Local Scope quotient_scope. +Local Open Scope ring_scope. +Local Open Scope quotient_scope. Reserved Notation "{ 'ratio' T }" (at level 0, format "{ 'ratio' T }"). Reserved Notation "{ 'fraction' T }" (at level 0, format "{ 'fraction' T }"). |