]> matita.cs.unibo.it Git - helm.git/commitdiff
recursive argument in let rec is not printed explicitly.
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 18 Jul 2007 11:17:46 +0000 (11:17 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 18 Jul 2007 11:17:46 +0000 (11:17 +0000)
I let to ferruccio optimize the case in which there is only one argument or the recno is 0 and thus can be omitted

components/content_pres/termContentPres.ml

index 6b3dcc297689783fbe1a99459cc287764c5d0511..110c78e46e43820fc4ae280e80090f9b35c40544 100644 (file)
@@ -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]) @