X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcontent_pres%2FtermContentPres.ml;h=110c78e46e43820fc4ae280e80090f9b35c40544;hb=1fa0edadead8eff6808429323c634171f44dc50f;hp=9f720e33b9a29740d414f6b5a0cd0d793ae0f2ef;hpb=9642ec8492f2ef54e280e27a40c2936a02c252f9;p=helm.git

diff --git a/components/content_pres/termContentPres.ml b/components/content_pres/termContentPres.ml
index 9f720e33b..110c78e46 100644
--- a/components/content_pres/termContentPres.ml
+++ b/components/content_pres/termContentPres.ml
@@ -202,21 +202,23 @@ let pp_ast0 t k =
               keyword "let"; space;
               hvbox false true [
                 aux_var var; space; builtin_symbol "\\def"; break; top_pos (k s) ];
-              break; keyword "in" ];
+              break; space; keyword "in" ];
             break;
             k t ])
     | Ast.LetRec (rec_kind, funs, where) ->
         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]) @