X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicUtil.ml;h=9b6ece214f4d1d251c28f85b25e82c3613c058fb;hb=f59b591eb48a06518b34d7f809bee51989307404;hp=36f65391eeac23d27c565b65d8e09ea52cd22f0c;hpb=2e58d03db0222ac0d885abeaebceac07ac586761;p=helm.git

diff --git a/helm/software/components/cic/cicUtil.ml b/helm/software/components/cic/cicUtil.ml
index 36f65391e..9b6ece214 100644
--- a/helm/software/components/cic/cicUtil.ml
+++ b/helm/software/components/cic/cicUtil.ml
@@ -622,11 +622,12 @@ let pp_rel out c i =
       | Some (s, _)    -> out (Printf.sprintf "%u[" i); pp_name out s; out "]"
    with Failure "nth" -> out (Printf.sprintf "%u[%i]" i (List.length c - i))
 
-let pp_implict out = function
+let pp_implicit out = function
    | None         -> out "?"
    | Some `Closed -> out "?[Closed]" 
    | Some `Type   -> out "?[Type]"
    | Some `Hole   -> out "?[Hole]"
+   | Some `Vector -> out "?[...]"
 
 let pp_uri out a =
    out (Printf.sprintf "%s<%s>" (UM.name_of_uri a) (UM.string_of_uri a)) 
@@ -634,7 +635,7 @@ let pp_uri out a =
 let rec pp_term out e c = function
    | C.Sort h                      -> pp_sort out h
    | C.Rel i                       -> pp_rel out c i
-   | C.Implicit x                  -> pp_implict out x
+   | C.Implicit x                  -> pp_implicit out x
    | C.Meta (i, iss)               ->
       let map = function None   -> out "_" | Some v -> pp_term out e c v in
       out (Printf.sprintf "?%u" i); xiter out "[" "; " "]" map iss