aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/g_vernac.ml4
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 /vernac/g_vernac.ml4
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 'vernac/g_vernac.ml4')
-rw-r--r--vernac/g_vernac.ml44
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4
index 3a59242de..16934fc86 100644
--- a/vernac/g_vernac.ml4
+++ b/vernac/g_vernac.ml4
@@ -549,7 +549,7 @@ GEXTEND Gram
] ]
;
module_expr_atom:
- [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (qid.CAst.v) | "("; me = module_expr; ")" -> me ] ]
+ [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident qid | "("; me = module_expr; ")" -> me ] ]
;
with_declaration:
[ [ "Definition"; fqid = fullyqualid; udecl = OPT univ_decl; ":="; c = Constr.lconstr ->
@@ -559,7 +559,7 @@ GEXTEND Gram
] ]
;
module_type:
- [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (qid.CAst.v)
+ [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident qid
| "("; mt = module_type; ")" -> mt
| mty = module_type; me = module_expr_atom ->
CAst.make ~loc:!@loc @@ CMapply (mty,me)