From 42ff3109217452853c3b853d21f09a317dd6e37d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 10 Jun 2019 23:11:06 +0200
Subject: [library] Move `Declaremods` to `vernac/`

We move `Declaremods` to the vernac layer as it implement
vernac-specific logic to manipulate modules which moreover is highly
imperative.

This forces code [such as printing] to manipulate the _global
imperative_ state which is a bit fishy.

The key improvement in this PR is that now `Global` is not used
anymore in `library`, so we can proceed to move it upwards.

This move is a follow-up of #10562 and a step towards moving `Global`
upper, likely to `interp` in the short term.
---
 interp/modintern.ml  | 6 +++---
 interp/modintern.mli | 4 +++-
 2 files changed, 6 insertions(+), 4 deletions(-)

(limited to 'interp')

diff --git a/interp/modintern.ml b/interp/modintern.ml
index 955288244e..ddf5b2d7b1 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -12,7 +12,6 @@ open Declarations
 open Libnames
 open Constrexpr
 open Constrintern
-open Declaremods
 
 type module_internalization_error =
   | NotAModuleNorModtype of string
@@ -21,9 +20,11 @@ type module_internalization_error =
 
 exception ModuleInternalizationError of module_internalization_error
 
+type module_kind = Module | ModType | ModAny
+
 let error_not_a_module_loc kind loc qid =
   let s = string_of_qualid qid in
-  let e = let open Declaremods in match kind with
+  let e = match kind with
     | Module -> Modops.ModuleTypingError (Modops.NotAModule s)
     | ModType -> Modops.ModuleTypingError (Modops.NotAModuleType s)
     | ModAny -> ModuleInternalizationError (NotAModuleNorModtype s)
@@ -46,7 +47,6 @@ let error_application_to_module_type loc =
     it is equal to the input kind when this one isn't ModAny. *)
 
 let lookup_module_or_modtype kind qid =
-  let open Declaremods in
   let loc = qid.CAst.loc in
   try
     if kind == ModType then raise Not_found;
diff --git a/interp/modintern.mli b/interp/modintern.mli
index 75ab38c64a..72695a680e 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -28,5 +28,7 @@ exception ModuleInternalizationError of module_internalization_error
    kind is never ModAny, and it is equal to the input kind when this one
    isn't ModAny. *)
 
+type module_kind = Module | ModType | ModAny
+
 val interp_module_ast :
-  env -> Declaremods.module_kind -> module_ast -> module_struct_entry * Declaremods.module_kind * Univ.ContextSet.t
+  env -> module_kind -> module_ast -> module_struct_entry * module_kind * Univ.ContextSet.t
-- 
cgit v1.2.3