From 0aa164f8fc8adf2cd57681ef64ff598c71b5d9f8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 31 Mar 2018 15:31:19 +0200
Subject: Declaring Scope prior to loading primitive printers.

---
 theories/Numbers/Cyclic/Int31/Int31.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'theories/Numbers')

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.
-- 
cgit v1.2.3