X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FtermContentPres.ml;h=c115fe018efb8d4698f8bea0c36cacf059f9521f;hb=651c5c55cba9ddbe592badc86b18502b83ecf580;hp=2544adb5d0deaec128f9d842a0768176f0a61e30;hpb=14e2489ae86ecb6467fe9a7ba3b742a8d53c47ea;p=helm.git

diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml
index 2544adb5d..c115fe018 100644
--- a/helm/software/components/content_pres/termContentPres.ml
+++ b/helm/software/components/content_pres/termContentPres.ml
@@ -253,7 +253,8 @@ let pp_ast0 t k =
           ((hvbox false false
             (fst_row :: List.flatten tl_rows
              @ [ break; keyword "in"; break; k where ])))
-    | Ast.Implicit -> builtin_symbol "?"
+    | Ast.Implicit `JustOne -> builtin_symbol "?"
+    | Ast.Implicit `Vector -> builtin_symbol "…"
     | Ast.Meta (n, l) ->
         let local_context l =
             List.map (function None -> None | Some t -> Some (k t)) l
@@ -596,7 +597,7 @@ let instantiate_level2 env term =
         Ast.Ident (name, Some (aux_substs env substs))
     | Ast.Meta (index, substs) -> Ast.Meta (index, aux_meta_substs env substs)
 
-    | Ast.Implicit
+    | Ast.Implicit _
     | Ast.Ident _
     | Ast.Num _
     | Ast.Sort _