From bb438b1c68febb34c85bbe2a2d39914e4c4cf53e Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 6 Sep 2005 16:47:29 +0000
Subject: [PATCH] uses \def symbol for definitions in context

---
 helm/ocaml/cic_transformations/sequent2pres.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
2.39.2