diff options
| author | Hugo Herbelin | 2020-09-27 10:46:48 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-10 22:16:39 +0200 |
| commit | a6d52d2502c09e8acdca464faf67d3956448cbcf (patch) | |
| tree | 71bf5602781c1e21a90d84555d8b62068fc31149 /parsing/g_constr.mlg | |
| parent | b7c9ba2c678228593450ecdf272ff71facbc6a6e (diff) | |
Prim.pattern_ident takes a location and its synonymous pattern_identref is deprecated.
Diffstat (limited to 'parsing/g_constr.mlg')
| -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 931ffccb27..644493a010 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -154,7 +154,7 @@ GRAMMAR EXTEND Gram | "10" LEFTA [ f = operconstr; args = LIST1 appl_arg -> { CAst.make ~loc @@ CApp((None,f),args) } | "@"; f = global; i = univ_instance; args = LIST0 NEXT -> { CAst.make ~loc @@ CAppExpl((None,f,i),args) } - | "@"; lid = pattern_identref; args = LIST1 identref -> + | "@"; lid = pattern_ident; args = LIST1 identref -> { let { CAst.loc = locid; v = id } = lid in let args = List.map (fun x -> CAst.make @@ CRef (qualid_of_ident ?loc:x.CAst.loc x.CAst.v, None), None) args in CAst.make ~loc @@ CApp((None, CAst.make ?loc:locid @@ CPatVar id),args) } ] @@ -262,8 +262,8 @@ GRAMMAR EXTEND Gram | s = string -> { CAst.make ~loc @@ CPrim (String s) } | "_" -> { CAst.make ~loc @@ CHole (None, IntroAnonymous, 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_identref; inst = evar_instance -> { CAst.make ~loc @@ CEvar(id,inst) } ] ] + | "?"; "["; id = pattern_ident; "]" -> { CAst.make ~loc @@ CHole (None, IntroFresh id.CAst.v, None) } + | id = pattern_ident; inst = evar_instance -> { CAst.make ~loc @@ CEvar(id,inst) } ] ] ; inst: [ [ id = identref; ":="; c = lconstr -> { (id,c) } ] ] |