diff options
| -rw-r--r-- | toplevel/metasyntax.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 604f32198d..f9b315842e 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -141,14 +141,15 @@ let infix_syntax_entry assoc n inf pref = | Some(Gramext.LeftA) -> (Extend.E,Extend.L) | Some(Gramext.NonA) -> (Extend.L,Extend.L) | None -> (Extend.E,Extend.L) (* LEFTA by default *) - in + in + let astref = Astterm.globalize_constr (Nvar ((0,0), pref)) in [{Extend.syn_id = pref^"_infix"; Extend.syn_prec = n,0,0; Extend.syn_astpat = Pnode ("APPLIST", Pcons - (Pquote (Nvar ((0, 0), pref)), + (Pquote astref, Pcons (Pmeta ("$e1", Tany), Pcons (Pmeta ("$e2", Tany), Pnil)))); Extend.syn_hunks = [Extend.UNP_BOX |