From: Enrico Tassi Date: Wed, 18 Jul 2007 11:17:46 +0000 (+0000) Subject: recursive argument in let rec is not printed explicitly. X-Git-Tag: 0.4.95@7852~312 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a08e3ef37c9bbbc977da6295787db5944182ce92;p=helm.git recursive argument in let rec is not printed explicitly. I let to ferruccio optimize the case in which there is only one argument or the recno is 0 and thus can be omitted --- diff --git a/components/content_pres/termContentPres.ml b/components/content_pres/termContentPres.ml index 6b3dcc297..110c78e46 100644 --- a/components/content_pres/termContentPres.ml +++ b/components/content_pres/termContentPres.ml @@ -209,14 +209,16 @@ let pp_ast0 t k = 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; @@ -224,6 +226,7 @@ let pp_ast0 t k = space; name] @ params @ + [space; keyword "on" ; space ; rec_param ;space ] @ (match ty with None -> [] | Some ty -> [builtin_symbol ":"; ty]) @ [ builtin_symbol "\\def"; break; @@ -231,12 +234,13 @@ let pp_ast0 t k = 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]) @