From bb438b1c68febb34c85bbe2a2d39914e4c4cf53e Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli 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