From d2257170c1c175e956db731bd3ecea084538b4d9 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 17 Oct 2003 15:46:44 +0000
Subject: Bug des terminaux quotés

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4666 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/metasyntax.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 18dc7366b5..f1ceda650a 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -494,7 +494,7 @@ let hunks_of_format (from,(vars,typs) as vt) symfmt =
       when s' = String.make (String.length s') ' ' ->
       let symbs, l = aux (symbs,fmt) in symbs, u :: l
   | Terminal s :: symbs, (UnpTerminal s' as u) :: fmt when quote s = s' ->
-      let symbs, l = aux (symbs,fmt) in symbs, u :: l
+      let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l
   | NonTerminal s :: symbs, UnpTerminal s' :: fmt when s = id_of_string s' ->
       let i = list_index s vars in
       let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in
-- 
cgit v1.2.3