X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2Fprint_grammar.ml;h=f05b77a11b029fa75d60ea5d920793ebca2767fa;hb=ac31c84bb9bcf327554976d4296d787853fc8db5;hp=6a05865de8f2c9149b6e6a6c6e7ca4b274afd315;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/grafite_parser/print_grammar.ml b/helm/software/components/grafite_parser/print_grammar.ml
index 6a05865de..f05b77a11 100644
--- a/helm/software/components/grafite_parser/print_grammar.ml
+++ b/helm/software/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