diff options
Diffstat (limited to 'theories/Reals')
| -rw-r--r-- | theories/Reals/RIneq.v | 4 | ||||
| -rw-r--r-- | theories/Reals/Rtrigo.v | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 8823e5d5be..55e3896a80 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -19,8 +19,8 @@ Require Export ZArithRing. Require Import Omega. Require Export RealField. -Open Local Scope Z_scope. -Open Local Scope R_scope. +Local Open Scope Z_scope. +Local Open Scope R_scope. Implicit Type r : R. diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index 2f69fb7616..c9f83d639a 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -19,8 +19,8 @@ Require Export Cos_plus. Require Import ZArith_base. Require Import Zcomplements. Require Import Classical_Prop. -Open Local Scope nat_scope. -Open Local Scope R_scope. +Local Open Scope nat_scope. +Local Open Scope R_scope. (** sin_PI2 is the only remaining axiom **) Axiom sin_PI2 : sin (PI / 2) = 1. |