| Ast.Implicit -> builtin_symbol "?"
| Ast.Meta (n, l) ->
let local_context l =
- CicNotationUtil.dress (builtin_symbol ";")
- (List.map (function None -> builtin_symbol "_" | Some t -> k t) l)
+ List.map (function None -> None | Some t -> Some (k t)) l
in
- hbox false false
- ([ builtin_symbol "?"; number (string_of_int n) ]
- @ (if l <> [] then local_context l else []))
+ Ast.Meta(n, local_context l)
| Ast.Sort sort -> aux_sort sort
| Ast.Num _
| Ast.Symbol _