From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 6 Sep 2005 16:47:29 +0000 (+0000)
Subject: uses \def symbol for definitions in context
X-Git-Tag: V_0_1_2_1~71
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bb438b1c68febb34c85bbe2a2d39914e4c4cf53e;p=helm.git

uses \def symbol for definitions in context
---

diff --git a/helm/ocaml/cic_transformations/sequent2pres.ml b/helm/ocaml/cic_transformations/sequent2pres.ml
index bac0f1509..b7de8499a 100644
--- 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