X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2Fprint_grammar.ml;h=f05b77a11b029fa75d60ea5d920793ebca2767fa;hb=249d11773d32add20d665c4f8521b7380e4fec0a;hp=6a05865de8f2c9149b6e6a6c6e7ca4b274afd315;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/grafite_parser/print_grammar.ml b/components/grafite_parser/print_grammar.ml
index 6a05865de..f05b77a11 100644
--- a/components/grafite_parser/print_grammar.ml
+++ b/components/grafite_parser/print_grammar.ml
@@ -28,11 +28,15 @@
 open Gramext 
 
 let tex_of_unicode s =
+(*CSC: ??????? What's the meaning of this function?
   let contractions = ("\\Longrightarrow","=>") :: [] in
   if String.length s <= 1 then s
   else  (* probably an extended unicode symbol *)
     let s = Utf8Macro.tex_of_unicode s in
     try List.assoc s contractions with Not_found -> s
+*) match Utf8Macro.tex_of_unicode s with
+      Some s -> s
+    | None -> s
 
 let needs_brackets t =
   let rec count_brothers = function