From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 13 Oct 2006 16:59:04 +0000 (+0000)
Subject: Content level representation of LetRec changed.
X-Git-Tag: make_still_working~6749
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3bd924d184cda530c75cbbc6b6afcdfe91080e71;p=helm.git

Content level representation of LetRec changed.
---

diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml
index 96a15c01e..e925db0aa 100644
--- a/helm/software/components/content_pres/termContentPres.ml
+++ b/helm/software/components/content_pres/termContentPres.ml
@@ -206,23 +206,36 @@ let pp_ast0 t k =
         let rec_op =
           match rec_kind with `Inductive -> "rec" | `CoInductive -> "corec"
         in
-        let mk_fun (var, body, _) = aux_var var, k body 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_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 (name, body) = fst_fun in
-          hvbox false true [
-            keyword "let"; keyword rec_op; name; builtin_symbol "\\def"; break;
-            top_pos body ]
+          let (params, name, ty, body) = fst_fun in
+          hvbox false true ([
+            keyword "let";
+            keyword rec_op;
+            name] @
+            params @
+            (match ty with None -> [] | Some ty -> [builtin_symbol ":"; ty]) @
+            [ builtin_symbol "\\def";
+            break;
+            top_pos body ])
         in
         let tl_rows =
           List.map
-            (fun (name, body) ->
+            (fun (params, name, ty, body) ->
               [ break;
-                hvbox false true [
-                  keyword "and"; name; builtin_symbol "\\def"; break; body ] ])
+                hvbox false true ([
+                  keyword "and";
+                  name] @
+                  params @
+                  (match ty with
+                      None -> []
+                    | Some ty -> [builtin_symbol ":"; ty]) @
+                  [ builtin_symbol "\\def"; break; body ])])
             tl_funs
         in
         add_level_info Ast.let_in_prec Ast.let_in_assoc
@@ -555,8 +568,8 @@ let instantiate_level2 env 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_definition env (var, term, i) =
-    (aux_capture_var env var, aux env term, i)
+  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 =
     List.map (fun (name, term) -> (name, aux env term)) substs
   and aux_meta_substs env meta_substs = List.map (aux_opt env) meta_substs