aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_vernac.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/g_vernac.ml4')
-rw-r--r--parsing/g_vernac.ml44
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f1ec49623..99eec9742 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -554,7 +554,7 @@ GEXTEND Gram
] ]
;
module_expr_atom:
- [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (snd qid) | "("; me = module_expr; ")" -> me ] ]
+ [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (qid.CAst.v) | "("; me = module_expr; ")" -> me ] ]
;
with_declaration:
[ [ "Definition"; fqid = fullyqualid; udecl = OPT univ_decl; ":="; c = Constr.lconstr ->
@@ -564,7 +564,7 @@ GEXTEND Gram
] ]
;
module_type:
- [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (snd qid)
+ [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (qid.CAst.v)
| "("; mt = module_type; ")" -> mt
| mty = module_type; me = module_expr_atom ->
CAst.make ~loc:!@loc @@ CMapply (mty,me)