X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationPp.ml;h=c2ee6a776cba5d8d223b99ec9bf3eecf7d77d1e9;hb=a90c31c1b53222bd6d57360c5ba5c2d0fe7d5207;hp=f94891375fa7adddf8be10dc2d817692ae594270;hpb=4377e950998c9c63937582952a79975947aa9a45;p=helm.git

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index f94891375..c2ee6a776 100644
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/components/acic_content/cicNotationPp.ml
@@ -144,8 +144,8 @@ let rec pp_term ?(pp_parens = true) t =
     | Ast.Ident (name, Some substs)
     | Ast.Uri (name, Some substs) ->
         sprintf "%s \\subst [%s]" name (pp_substs substs)
-    | Ast.Implicit `Vector -> "…"
-    | Ast.Implicit `JustOne -> "?"
+    | Ast.Implicit `Vector -> "?"
+    | Ast.Implicit `JustOne -> "…"
     | Ast.Implicit (`Tagged name) -> "?"^name
     | Ast.Meta (index, substs) ->
         sprintf "%d[%s]" index
@@ -160,7 +160,7 @@ let rec pp_term ?(pp_parens = true) t =
     | Ast.Sort (`NCProp s)-> "CProp[" ^ s ^ "]"
     | Ast.Symbol (name, _) -> "'" ^ name
 
-    | Ast.UserInput -> "%"
+    | Ast.UserInput -> ""
 
     | Ast.Literal l -> pp_literal l
     | Ast.Layout l -> pp_layout l
@@ -170,7 +170,6 @@ let rec pp_term ?(pp_parens = true) t =
   match pp_parens, t with
     | false, _ 
     | true, Ast.Implicit _
-    | true, Ast.UserInput
     | true, Ast.Sort _
     | true, Ast.Ident (_, Some []) 
     | true, Ast.Ident (_, None)    -> t_pp