aboutsummaryrefslogtreecommitdiff
path: root/src/boot/fe/item.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/boot/fe/item.ml')
-rw-r--r--src/boot/fe/item.ml14
1 files changed, 11 insertions, 3 deletions
diff --git a/src/boot/fe/item.ml b/src/boot/fe/item.ml
index b5a8bb7a..91a0c3dd 100644
--- a/src/boot/fe/item.ml
+++ b/src/boot/fe/item.ml
@@ -786,9 +786,17 @@ and parse_mod_item (ps:pstate) : (Ast.ident * Ast.mod_item) =
EQ ->
begin
bump ps;
- match peek ps with
- LIT_STR s -> (bump ps; s)
- | _ -> raise (unexpected ps)
+ let do_tok t =
+ bump ps;
+ match t with
+ LIT_STR s -> s
+ | _ -> raise (unexpected ps)
+ in
+ match peek ps with
+ IDENT i ->
+ do_tok (ps.pstate_get_cenv_tok ps i)
+ | t ->
+ do_tok t
end
| _ -> ps.pstate_infer_lib_name ident
in