From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 18 Jul 2008 12:51:05 +0000 (+0000)
Subject: metavariable context has a separator now
X-Git-Tag: make_still_working~4914
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b637879a2b3f2ceda65afb3c950061189c4730b7;p=helm.git

metavariable context has a separator now
---

diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index f7b7067cc..8fe5657b3 100644
--- a/helm/software/components/content_pres/content2pres.ml
+++ b/helm/software/components/content_pres/content2pres.ml
@@ -815,7 +815,9 @@ let conjecture2pres term2pres (id, n, context, ty) =
   (B.b_hv [Some "helm", "xref", id]
      ((B.b_toggle [
         B.b_h [] [B.b_text [] "{...}"; B.b_space];
-        B.b_hv [] (List.map
+        B.b_hv [] (HExtlib.list_concat ~sep:[B.b_text [] ";"; B.b_space] 
+         (List.map (fun x -> [x])
+         (List.map
           (function
              | None ->
 		 B.b_h []
@@ -856,7 +858,7 @@ let conjecture2pres term2pres (id, n, context, ty) =
 					| Some n -> n)) ;
                        B.b_text [] (Utf8Macro.unicode_of_tex "\\Assign");
                        proof2pres true term2pres p])
-          (List.rev context)) ] ::
+          (List.rev context)))) ] ::
          [ B.b_h []
            [ B.b_text [] (Utf8Macro.unicode_of_tex "\\vdash");
              B.b_object (p_mi [] (string_of_int n)) ;