X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationPp.ml;h=1e759930ac4ef706175c85c181244657e3dd5558;hb=d34061fd1c820139fad38c39dee6377e5057bf26;hp=5eb6b64d2ad26fd1c27a3904bb94126a12176b22;hpb=ee7855524284ea3a282c68f22ffa36e535a11810;p=helm.git

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index 5eb6b64d2..1e759930a 100644
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/components/acic_content/cicNotationPp.ml
@@ -117,14 +117,14 @@ let rec pp_term ?(pp_parens = true) t =
           (pp_term ~pp_parens:true t3)
     | Ast.LetRec (kind, definitions, term) ->
 	let rec get_guard i = function
-	   | []                   -> (*assert false*) Ast.Implicit
+	   | []                   -> (*assert false*) Ast.Implicit `JustOne
 	   | [term, _] when i = 1 -> term
 	   | _ :: tl              -> get_guard (pred i) tl
 	in
 	let map (params, (id,typ), body, i) =
          let typ =
           match typ with
-             None -> Ast.Implicit
+             None -> Ast.Implicit `JustOne
            | Some typ -> typ
          in
 	   sprintf "%s %s on %s: %s \\def %s" 
@@ -143,7 +143,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 -> "?"
+    | Ast.Implicit `Vector -> "?"
+    | Ast.Implicit `JustOne -> "..."
     | Ast.Meta (index, substs) ->
         sprintf "%d[%s]" index
           (String.concat "; "
@@ -166,7 +167,7 @@ let rec pp_term ?(pp_parens = true) t =
   in
   match pp_parens, t with
     | false, _ 
-    | true, Ast.Implicit
+    | true, Ast.Implicit _
     | true, Ast.Sort _
     | true, Ast.Ident (_, Some []) 
     | true, Ast.Ident (_, None)    -> t_pp