]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/content_pres/termContentPres.ml
"..." -> "\ldots" for implicit vectors
[helm.git] / helm / software / components / content_pres / termContentPres.ml
index 5e8f26a4f7758deb8816c37633b97e0b2b2d15b7..c115fe018efb8d4698f8bea0c36cacf059f9521f 100644 (file)
@@ -254,7 +254,7 @@ let pp_ast0 t k =
             (fst_row :: List.flatten tl_rows
              @ [ break; keyword "in"; break; k where ])))
     | Ast.Implicit `JustOne -> builtin_symbol "?"
-    | Ast.Implicit `Vector -> 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