From 4f0bdf2e19f0562a6cdf3b5ac075326b6e28c1d7 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 2 Jul 2019 13:02:57 +0200
Subject: Move declare_universe_context to top of Declare

In preparation for the other declarations to use it.
---
 tactics/declare.ml | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

diff --git a/tactics/declare.ml b/tactics/declare.ml
index ed745b1269..d93fcc0950 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -33,6 +33,19 @@ module NamedDecl = Context.Named.Declaration
 
 type import_status = ImportDefaultBehavior | ImportNeedQualified
 
+(** Monomorphic universes need to survive sections. *)
+
+let input_universe_context : Univ.ContextSet.t -> Libobject.obj =
+  declare_object @@ local_object "Monomorphic section universes"
+    ~cache:(fun (na, uctx) -> Global.push_context_set false uctx)
+    ~discharge:(fun (_, x) -> Some x)
+
+let declare_universe_context ~poly ctx =
+  if poly then
+    (Global.push_context_set true ctx; Lib.add_section_context ctx)
+  else
+    Lib.add_anonymous_leaf (input_universe_context ctx)
+
 (** Declaration of constants and parameters *)
 
 type constant_obj = {
@@ -553,19 +566,6 @@ let assumption_message id =
   discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *)
   Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared")
 
-(** Monomorphic universes need to survive sections. *)
-
-let input_universe_context : Univ.ContextSet.t -> Libobject.obj =
-  declare_object @@ local_object "Monomorphic section universes"
-    ~cache:(fun (na, uctx) -> Global.push_context_set false uctx)
-    ~discharge:(fun (_, x) -> Some x)
-
-let declare_universe_context ~poly ctx =
-  if poly then
-    (Global.push_context_set true ctx; Lib.add_section_context ctx)
-  else
-    Lib.add_anonymous_leaf (input_universe_context ctx)
-
 (** Global universes are not substitutive objects but global objects
    bound at the *library* or *module* level. The polymorphic flag is
    used to distinguish universes declared in polymorphic sections, which
-- 
cgit v1.2.3