diff options
| author | Hugo Herbelin | 2020-04-27 14:39:56 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-10 22:13:59 +0200 |
| commit | 2cf0287c9c863d7969fb5d4e85b7ca538dd103c2 (patch) | |
| tree | 0dfa98a20514443017dcd81d165cdcb494e5743f /parsing | |
| parent | 03d55f990bb7a2c4f5c1fefa408b94a8a93e8d05 (diff) | |
Adding and using locations on identifiers in constr_expr where they were missing.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.mlg | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 1ec83c496a..df2de3333d 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -252,7 +252,7 @@ GRAMMAR EXTEND Gram | "cofix"; c = cofix_decls -> { let (id,dcls) = c in CAst.make ~loc @@ CCoFix (id,dcls) } ] ] ; appl_arg: - [ [ test_lpar_id_coloneq; "("; id = ident; ":="; c = lconstr; ")" -> { (c,Some (CAst.make ~loc @@ ExplByName id)) } + [ [ test_lpar_id_coloneq; "("; id = identref; ":="; c = lconstr; ")" -> { (c,Some (CAst.make ?loc:id.CAst.loc @@ ExplByName id.CAst.v)) } | c=operconstr LEVEL "9" -> { (c,None) } ] ] ; atomic_constr: @@ -261,12 +261,12 @@ GRAMMAR EXTEND Gram | n = NUMBER-> { CAst.make ~loc @@ CPrim (Numeral (NumTok.SPlus,n)) } | s = string -> { CAst.make ~loc @@ CPrim (String s) } | "_" -> { CAst.make ~loc @@ CHole (None, IntroAnonymous, None) } - | "?"; "["; id = ident; "]" -> { CAst.make ~loc @@ CHole (None, IntroIdentifier id, None) } + | "?"; "["; id = identref; "]" -> { CAst.make ~loc @@ CHole (None, IntroIdentifier id.CAst.v, None) } | "?"; "["; id = pattern_ident; "]" -> { CAst.make ~loc @@ CHole (None, IntroFresh id, None) } | id = pattern_ident; inst = evar_instance -> { CAst.make ~loc @@ CEvar(id,inst) } ] ] ; inst: - [ [ id = ident; ":="; c = lconstr -> { (id,c) } ] ] + [ [ id = identref; ":="; c = lconstr -> { (id,c) } ] ] ; evar_instance: [ [ "@{"; l = LIST1 inst SEP ";"; "}" -> { l } |