From a4da3fbec91ee28596c34414b6c58eb1e19b4f78 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 16 Oct 2000 21:18:25 +0000
Subject: Correction bug affichage des infix

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@710 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/metasyntax.ml | 5 +++--
 1 file 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
-- 
cgit v1.2.3