diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-17 15:46:44 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-17 15:46:44 +0000 |
| commit | d2257170c1c175e956db731bd3ecea084538b4d9 (patch) | |
| tree | bd1b10a9ddf4736d96ae2d3ad582cc0d8d6f885c /toplevel/metasyntax.ml | |
| parent | 717cc0231fe121cf2e6917b582374bbf67e0b676 (diff) | |
Bug des terminaux quotés
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4666 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/metasyntax.ml')
| -rw-r--r-- | toplevel/metasyntax.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 18dc7366b..f1ceda650 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 |