aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-21 20:48:30 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-06-12 14:42:27 +0200
commit9367f1626afb080d10d425262dca705046a32933 (patch)
treed91633162c245239e50587e766b739194f094a57 /interp
parent2af78d3cca0f941841394b224b96f86903a68b10 (diff)
[api] Misctypes removal: module_kind to Declaremods
Diffstat (limited to 'interp')
-rw-r--r--interp/modintern.ml5
-rw-r--r--interp/modintern.mli3
2 files changed, 4 insertions, 4 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