| `CProp _ -> "CProp"
| `Type _ -> "Type"
| `NType s -> "Type[" ^ s ^ "]"
+ | `NCProp s -> "CProp[" ^ s ^ "]"
let map_space f l =
HExtlib.list_concat
(fun (params, name, ty, body, rec_param) ->
[ break;
hvbox false true ([
- keyword "and";
+ keyword "and"; space;
name] @
params @
[space; keyword "on" ; space; rec_param ;space ] @
((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 _