diff options
Diffstat (limited to 'interp/modintern.ml')
| -rw-r--r-- | interp/modintern.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/interp/modintern.ml b/interp/modintern.ml index dc93d8dc..c27cc9cc 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) @@ -45,7 +45,9 @@ let error_application_to_module_type loc = or both are searched. The returned kind is never ModAny, and it is equal to the input kind when this one isn't ModAny. *) -let lookup_module_or_modtype kind {CAst.loc;v=qid} = +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; let mp = Nametab.locate_module qid in @@ -63,7 +65,7 @@ let transl_with_decl env = function | CWith_Module ({CAst.v=fqid},qid) -> WithMod (fqid,lookup_module qid), Univ.ContextSet.empty | CWith_Definition ({CAst.v=fqid},udecl,c) -> - let sigma, udecl = Univdecls.interp_univ_decl_opt env udecl in + let sigma, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in let c, ectx = interp_constr env sigma c in begin match UState.check_univ_decl ~poly:(Flags.is_universe_polymorphism()) ectx udecl with | Entries.Polymorphic_const_entry ctx -> @@ -83,7 +85,7 @@ let loc_of_module l = l.CAst.loc let rec interp_module_ast env kind m cst = match m with | {CAst.loc;v=CMident qid} -> - let (mp,kind) = lookup_module_or_modtype kind CAst.(make ?loc qid) in + let (mp,kind) = lookup_module_or_modtype kind qid in (MEident mp, kind, cst) | {CAst.loc;v=CMapply (me1,me2)} -> let me1',kind1, cst = interp_module_ast env kind me1 cst in |