diff options
| author | Emilio Jesus Gallego Arias | 2018-05-21 20:48:30 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-06-12 14:42:27 +0200 |
| commit | 9367f1626afb080d10d425262dca705046a32933 (patch) | |
| tree | d91633162c245239e50587e766b739194f094a57 /interp/modintern.ml | |
| parent | 2af78d3cca0f941841394b224b96f86903a68b10 (diff) | |
[api] Misctypes removal: module_kind to Declaremods
Diffstat (limited to 'interp/modintern.ml')
| -rw-r--r-- | interp/modintern.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/interp/modintern.ml b/interp/modintern.ml index fefd2ab6f5..33c07d5514 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 |