uses \def symbol for definitions in context

diff --git a/helm/ocaml/cic_transformations/sequent2pres.ml b/helm/ocaml/cic_transformations/sequent2pres.ml
index bac0f1509da11e12665461c105c54e8261b9c8d9..b7de8499a1404df236de4459ae606626ad73f7e2 100644 (file)
--- a/helm/ocaml/cic_transformations/sequent2pres.ml
+++ b/helm/ocaml/cic_transformations/sequent2pres.ml
@@ -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