From: Enrico Tassi <enrico.tassi@inria.fr>
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]) @