From 9367f1626afb080d10d425262dca705046a32933 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 21 May 2018 20:48:30 +0200
Subject: [api] Misctypes removal: module_kind to Declaremods

---
 interp/modintern.ml     | 5 +++--
 interp/modintern.mli    | 3 +--
 library/declaremods.ml  | 6 ++++--
 library/declaremods.mli | 8 ++++++--
 library/misctypes.ml    | 6 ------
 5 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/interp/modintern.ml b/interp/modintern.ml
index fefd2ab6f..33c07d551 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -12,7 +12,7 @@ open Declarations
 open Libnames
 open Constrexpr
 open Constrintern
-open Misctypes
+open Declaremods
 
 type module_internalization_error =
   | NotAModuleNorModtype of string
@@ -23,7 +23,7 @@ exception ModuleInternalizationError of module_internalization_error
 
 let error_not_a_module_loc kind loc qid =
   let s = string_of_qualid qid in
-  let e = match kind with
+  let e = let open Declaremods in match kind with
     | Module -> Modops.ModuleTypingError (Modops.NotAModule s)
     | ModType -> Modops.ModuleTypingError (Modops.NotAModuleType s)
     | ModAny -> ModuleInternalizationError (NotAModuleNorModtype s)
@@ -46,6 +46,7 @@ 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 {CAst.loc;v=qid} =
+  let open Declaremods in
   try
     if kind == ModType then raise Not_found;
     let mp = Nametab.locate_module qid in
diff --git a/interp/modintern.mli b/interp/modintern.mli
index ef37aead8..529c438c1 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -11,7 +11,6 @@
 open Environ
 open Entries
 open Constrexpr
-open Misctypes
 
 (** Module internalization errors *)
 
@@ -30,4 +29,4 @@ exception ModuleInternalizationError of module_internalization_error
    isn't ModAny. *)
 
 val interp_module_ast :
-  env -> module_kind -> module_ast -> module_struct_entry * module_kind * Univ.ContextSet.t
+  env -> Declaremods.module_kind -> module_ast -> module_struct_entry * Declaremods.module_kind * Univ.ContextSet.t
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 1d5df49cf..e8d89f96b 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -36,6 +36,8 @@ type inline =
   | DefaultInline
   | InlineAt of int
 
+type module_kind = Module | ModType | ModAny
+
 let default_inline () = Some (Flags.get_inline_level ())
 
 let inl2intopt = function
@@ -994,8 +996,8 @@ let iter_all_segments f =
 (** {6 Some types used to shorten declaremods.mli} *)
 
 type 'modast module_interpretor =
-  Environ.env -> Misctypes.module_kind -> 'modast ->
-    Entries.module_struct_entry * Misctypes.module_kind * Univ.ContextSet.t
+  Environ.env -> module_kind -> 'modast ->
+    Entries.module_struct_entry * module_kind * Univ.ContextSet.t
 
 type 'modast module_params =
   (lident list * ('modast * inline)) list
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 4aee7feae..63b25c7e4 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -27,9 +27,13 @@ type inline =
   | DefaultInline
   | InlineAt of int
 
+(** Kinds of modules *)
+
+type module_kind = Module | ModType | ModAny
+
 type 'modast module_interpretor =
-  Environ.env -> Misctypes.module_kind -> 'modast ->
-    Entries.module_struct_entry * Misctypes.module_kind * Univ.ContextSet.t
+  Environ.env -> module_kind -> 'modast ->
+    Entries.module_struct_entry * module_kind * Univ.ContextSet.t
 
 type 'modast module_params =
   (Misctypes.lident list * ('modast * inline)) list
diff --git a/library/misctypes.ml b/library/misctypes.ml
index ac8c7890c..a12caef80 100644
--- a/library/misctypes.ml
+++ b/library/misctypes.ml
@@ -75,7 +75,6 @@ type 'a bindings =
 
 type 'a with_bindings = 'a * 'a bindings
 
-
 (** Some utility types for parsing *)
 
 type 'a or_var =
@@ -93,11 +92,6 @@ type 'a or_by_notation = 'a or_by_notation_r CAst.t
 (* NB: the last string in [ByNotation] is actually a [Notation.delimiters],
    but this formulation avoids a useless dependency. *)
 
-
-(** Kinds of modules *)
-
-type module_kind = Module | ModType | ModAny
-
 (** Various flags *)
 
 type direction_flag = bool (* true = Left-to-right    false = right-to-right *)
-- 
cgit v1.2.3