diff options
| author | Gaëtan Gilbert | 2019-07-02 13:02:57 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-07-03 17:05:29 +0200 |
| commit | 4f0bdf2e19f0562a6cdf3b5ac075326b6e28c1d7 (patch) | |
| tree | 9c50f7bafd5bea50478483ea75bfd54fd88550b2 | |
| parent | bb81ed23c288f21f095d80a28ed7bda7ecf1a603 (diff) | |
Move declare_universe_context to top of Declare
In preparation for the other declarations to use it.
| -rw-r--r-- | tactics/declare.ml | 26 |
1 files 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 |