From c699a9669505947487dce49383fa50fe9b9968e8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 18 Jul 2008 12:55:24 +0000 Subject: [PATCH] better metavariable context --- helm/software/components/content_pres/content2pres.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml index 8fe5657b3..fc3a47b5e 100644 --- a/helm/software/components/content_pres/content2pres.ml +++ b/helm/software/components/content_pres/content2pres.ml @@ -835,7 +835,7 @@ let conjecture2pres term2pres (id, n, context, ty) = (match dec_name with None -> "_" | Some n -> n)); - B.b_text [] ":"; + B.b_text [] ":"; B.b_space; term2pres ty ] | Some (`Definition d) -> let @@ -848,6 +848,7 @@ let conjecture2pres term2pres (id, n, context, ty) = None -> "_" | Some n -> n)) ; B.b_text [] (Utf8Macro.unicode_of_tex "\\Assign"); + B.b_space; term2pres bo] | Some (`Proof p) -> let proof_name = p.Content.proof_name in @@ -857,12 +858,16 @@ let conjecture2pres term2pres (id, n, context, ty) = None -> "_" | Some n -> n)) ; B.b_text [] (Utf8Macro.unicode_of_tex "\\Assign"); + B.b_space; proof2pres true term2pres p]) (List.rev context)))) ] :: [ B.b_h [] - [ B.b_text [] (Utf8Macro.unicode_of_tex "\\vdash"); + [ B.b_space; + B.b_text [] (Utf8Macro.unicode_of_tex "\\vdash"); + B.b_space; B.b_object (p_mi [] (string_of_int n)) ; B.b_text [] ":" ; + B.b_space; term2pres ty ]]))) let metasenv2pres term2pres = function -- 2.39.2