| 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))
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