X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcontent_pres%2FtermContentPres.ml;h=0ee424f18570d318b74d942d936573029d206eed;hb=refs%2Ftags%2F0.4.95;hp=a8bfe114746f5c9d79968d7c96141de6d8f27646;hpb=f9512e878bd27f8cb5261bb18b0da0d42c8184d0;p=helm.git

diff --git a/components/content_pres/termContentPres.ml b/components/content_pres/termContentPres.ml
index a8bfe1147..0ee424f18 100644
--- a/components/content_pres/termContentPres.ml
+++ b/components/content_pres/termContentPres.ml
@@ -151,8 +151,11 @@ let pp_ast0 t k =
            space
          ]
         in
-        let mk_case_pattern (head, href, vars) =
-          hbox true false (ident_w_href href head :: List.map aux_var vars)
+        let mk_case_pattern =
+         function
+            Ast.Pattern (head, href, vars) ->
+             hbox true false (ident_w_href href head :: List.map aux_var vars)
+          | Ast.Wildcard -> builtin_symbol "_"
         in
         let patterns' =
           List.map
@@ -199,24 +202,26 @@ let pp_ast0 t k =
         add_level_info Ast.let_in_prec Ast.let_in_assoc
           (hvbox false true [
             hvbox false true [
-              keyword "let";
+              keyword "let"; space;
               hvbox false true [
-                aux_var var; builtin_symbol "\\def"; break; top_pos (k s) ];
-              break; keyword "in" ];
+                aux_var var; space; builtin_symbol "\\def"; break; top_pos (k s) ];
+              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 +229,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 +237,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]) @
@@ -571,8 +578,11 @@ let instantiate_level2 env term =
   and aux_capture_var env (name, ty_opt) = (aux env name, aux_opt env ty_opt)
   and aux_branch env (pattern, term) =
     (aux_pattern env pattern, aux env term)
-  and aux_pattern env (head, hrefs, vars) =
-    (head, hrefs, List.map (aux_capture_var env) vars)
+  and aux_pattern env =
+   function
+      Ast.Pattern (head, hrefs, vars) ->
+       Ast.Pattern (head, hrefs, List.map (aux_capture_var env) vars)
+    | Ast.Wildcard -> Ast.Wildcard
   and aux_definition env (params, var, term, i) =
     (List.map (aux_capture_var env) params, aux_capture_var env var, aux env term, i)
   and aux_substs env substs =