((hvbox false false
(fst_row :: List.flatten tl_rows
@ [ break; keyword "in"; break; k where ])))
- | Ast.Implicit -> builtin_symbol "?"
+ | Ast.Implicit `JustOne -> 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
Ast.Ident (name, Some (aux_substs env substs))
| Ast.Meta (index, substs) -> Ast.Meta (index, aux_meta_substs env substs)
- | Ast.Implicit
+ | Ast.Implicit _
| Ast.Ident _
| Ast.Num _
| Ast.Sort _