+let params2pres params =
+ let param2pres uri =
+ B.b_text [Some "xlink", "href", UriManager.string_of_uri uri]
+ (UriManager.name_of_uri uri)
+ in
+ let rec spatiate = function
+ | [] -> []
+ | hd :: [] -> [hd]
+ | hd :: tl -> hd :: B.b_text [] ", " :: spatiate tl
+ in
+ match params with
+ | [] -> []
+ | p ->
+ let params = spatiate (List.map param2pres p) in
+ [B.b_space;
+ B.b_h [] (B.b_text [] "[" :: params @ [ B.b_text [] "]" ])]
+
+let recursion_kind2pres params kind =
+ let kind =
+ match kind with
+ | `Recursive _ -> "Recursive definition"
+ | `CoRecursive -> "CoRecursive definition"
+ | `Inductive _ -> "Inductive definition"
+ | `CoInductive _ -> "CoInductive definition"
+ in
+ B.b_h [] (B.b_text [] kind :: params2pres params)
+
+let inductive2pres term2pres ind =
+ let constructor2pres decl =
+ B.b_h [] [
+ B.b_text [] ("| " ^ get_name decl.Content.dec_name ^ ":");
+ B.b_space;
+ term2pres decl.Content.dec_type
+ ]
+ in
+ B.b_v []
+ (B.b_h [] [
+ B.b_text [] (ind.Content.inductive_name ^ " of arity ");
+ term2pres ind.Content.inductive_type ]
+ :: List.map constructor2pres ind.Content.inductive_constructors)