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/Numbers | |
| parent | ace19eb0f555c6b2744bd23896e9459637d53394 (diff) | |
Declaring Scope prior to loading primitive printers.
Diffstat (limited to 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Int31.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index d91bfd4e2c..77ab624ca5 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -15,8 +15,6 @@ Require Import Wf_nat. Require Export ZArith. Require Export DoubleType. -Declare ML Module "int31_syntax_plugin". - (** * 31-bit integers *) (** This file contains basic definitions of a 31-bit integer @@ -51,6 +49,7 @@ Register digits as int31 bits in "coq_int31" by True. Register int31 as int31 type in "coq_int31" by True. Declare Scope int31_scope. +Declare ML Module "int31_syntax_plugin". Delimit Scope int31_scope with int31. Bind Scope int31_scope with int31. Local Open Scope int31_scope. |