]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/sequent2pres.ml
ocaml 3.09 transition
[helm.git] / helm / ocaml / cic_transformations / sequent2pres.ml
index bac0f1509da11e12665461c105c54e8261b9c8d9..b7de8499a1404df236de4459ae606626ad73f7e2 100644 (file)
@@ -76,7 +76,7 @@ let sequent2pres term2pres (_,_,context,ty) =
                 (match def_name with
                    None -> "_"
                  | Some n -> n)) ;
-                 Box.b_text [] ":=" ;
+                 Box.b_text [] (Utf8Macro.unicode_of_tex "\\def") ;
                 term2pres bo] in
          aux (r::accum) tl
       | _::_ -> assert false in