From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 interp/modintern.ml | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

(limited to 'interp/modintern.ml')

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
-- 
cgit v1.2.3