diff options
| author | herbelin | 2000-10-16 21:18:25 +0000 |
|---|---|---|
| committer | herbelin | 2000-10-16 21:18:25 +0000 |
| commit | a4da3fbec91ee28596c34414b6c58eb1e19b4f78 (patch) | |
| tree | 07421958ccaae5dfaf856a2084016f0aba6e06ac | |
| parent | 96b0f8fac2202a2593db285d97bebff5b379d684 (diff) | |
Correction bug affichage des infix
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@710 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |