aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/modintern.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-13 00:22:57 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-18 11:02:58 +0200
commit61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f (patch)
treec0d688ecee1d04f01f25a121cc3cc6ecabdfa1bc /interp/modintern.ml
parentf08153148b3ca0de01e5d7c68d5b318a2cae6d0d (diff)
Remove reference name type.
reference was defined as Ident or Qualid, but the qualid type already permits empty paths. So we had effectively two representations for unqualified names, that were not seen as equal by eq_reference. We remove the reference type and replace its uses by qualid.
Diffstat (limited to 'interp/modintern.ml')
-rw-r--r--interp/modintern.ml5
1 files changed, 3 insertions, 2 deletions
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 33c07d551..c27cc9cc0 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -45,8 +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
@@ -84,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