diff options
| -rw-r--r-- | interp/modintern.ml | 5 | ||||
| -rw-r--r-- | interp/modintern.mli | 3 | ||||
| -rw-r--r-- | library/declaremods.ml | 6 | ||||
| -rw-r--r-- | library/declaremods.mli | 8 | ||||
| -rw-r--r-- | 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 *) |