let rec_op =
match rec_kind with `Inductive -> "rec" | `CoInductive -> "corec"
in
- let mk_fun (args, (name,ty), body, _) =
- List.map aux_var args ,k name, HExtlib.map_option k ty, k body in
+ let mk_fun (args, (name,ty), body, rec_param) =
+ List.map aux_var args ,k name, HExtlib.map_option k ty, k body,
+ fst (List.nth args rec_param)
+ in
let mk_funs = List.map mk_fun in
let fst_fun, tl_funs =
match mk_funs funs with hd :: tl -> hd, tl | [] -> assert false
in
let fst_row =
- let (params, name, ty, body) = fst_fun in
+ let (params, name, ty, body, rec_param) = fst_fun in
hvbox false true ([
keyword "let";
space;
space;
name] @
params @
+ [space; keyword "on" ; space ; rec_param ;space ] @
(match ty with None -> [] | Some ty -> [builtin_symbol ":"; ty]) @
[ builtin_symbol "\\def";
break;
in
let tl_rows =
List.map
- (fun (params, name, ty, body) ->
+ (fun (params, name, ty, body, rec_param) ->
[ break;
hvbox false true ([
keyword "and";
name] @
params @
+ [space; keyword "on" ; space; rec_param ;space ] @
(match ty with
None -> []
| Some ty -> [builtin_symbol ":"; ty]) @