diff options
| author | Hugo Herbelin | 2018-03-31 15:31:19 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-10 19:56:28 +0200 |
| commit | 0aa164f8fc8adf2cd57681ef64ff598c71b5d9f8 (patch) | |
| tree | f9d9ecbdb9d4103d6d70ef84f29bafd3e8ae88fd /theories/Reals | |
| parent | ace19eb0f555c6b2744bd23896e9459637d53394 (diff) | |
Declaring Scope prior to loading primitive printers.
Diffstat (limited to 'theories/Reals')
| -rw-r--r-- | theories/Reals/Rdefinitions.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v index 857b4ec33b..932fcddaf5 100644 --- a/theories/Reals/Rdefinitions.v +++ b/theories/Reals/Rdefinitions.v @@ -12,12 +12,15 @@ (** Definitions for the axiomatization *) (*********************************************************) -Declare ML Module "r_syntax_plugin". Require Export ZArith_base. Parameter R : Set. -(* Declare Scope positive_scope with Key R *) +(* Declare primitive numeral notations for Scope R_scope *) +Declare Scope R_scope. +Declare ML Module "r_syntax_plugin". + +(* Declare Scope R_scope with Key R *) Delimit Scope R_scope with R. (* Automatically open scope R_scope for arguments of type R *) |