diff options
Diffstat (limited to 'parsing/g_prim.ml4')
| -rw-r--r-- | parsing/g_prim.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 524e7b468..0e91fddbd 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -71,7 +71,7 @@ GEXTEND Gram ; basequalid: [ [ id = ident; (l,id')=fields -> local_make_qualid (l@[id]) id' - | id = ident -> make_short_qualid id + | id = ident -> qualid_of_ident id ] ] ; name: |