diff options
Diffstat (limited to 'theories/Reals')
| -rw-r--r-- | theories/Reals/Rdefinitions.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v index 620400d61..26857c81f 100644 --- a/theories/Reals/Rdefinitions.v +++ b/theories/Reals/Rdefinitions.v @@ -17,6 +17,10 @@ Require Export ZArith_base. Require Export TypeSyntax. Parameter R:Type. + +Delimits Scope R_scope with R. +Bind Scope R_scope with R. + Parameter R0:R. Parameter R1:R. Parameter Rplus:R->R->R. |