Merge branch 'master' of ssh://matita.cs.unibo.it:/srv/git/helm

[helm.git] / matita / components / content_pres / content2pres.ml

diff --git a/matita/components/content_pres/content2pres.ml b/matita/components/content_pres/content2pres.ml
index d07733a1670676435894cb91528c20c084bafc83..880024ad9386491fd97ca48628b7fe61c7a8b4da 100644 (file)
--- a/matita/components/content_pres/content2pres.ml
+++ b/matita/components/content_pres/content2pres.ml
@@ -901,8 +901,10 @@ let definition2pres ?recno term2pres d =
   let rno = match recno with None -> -1 (* cofix *) | Some x -> x in
   let ty = d.Content.def_type in
   let module P = NotationPt in
-  let rec split_pi i t = 
-    if i <= 1 then 
+  let rec split_pi i t =
+    (* dummy case for corecursive defs *)
+    if i = ~-1 then [], P.UserInput, t
+    else if i <= 1 then 
       match t with 
       | P.Binder ((`Pi|`Forall),(var,_ as v),t) 
       | P.AttributedTerm (_,P.Binder ((`Pi|`Forall),(var,_ as v),t)) -> 
@@ -930,7 +932,9 @@ let definition2pres ?recno term2pres d =
   B.b_hv [] 
    [B.b_hov (RenderingAttrs.indent_attributes `BoxML)
     ( [B.b_hov (RenderingAttrs.indent_attributes `BoxML) ([ B.b_space; B.b_text [] name ] @ 
-        [B.indent(B.b_hov (RenderingAttrs.indent_attributes `BoxML) (params))])] 
+        if params <> [] then
+           [B.indent(B.b_hov (RenderingAttrs.indent_attributes `BoxML) (params))]
+        else [])] 
       @ [B.b_h [] 
          ((if rno <> -1 then 
            [B.b_kw "on";B.b_space;term2pres rec_param] else [])
@@ -1047,13 +1051,14 @@ let nconjlist2pres0 term2pres context =
           Con.dec_id = dec_id ;
           Con.dec_type = ty } = d in
       let r = 
-        Box.b_h [Some "helm", "xref", dec_id] 
-          [ Box.b_object (p_mi []
-            (match dec_name with
-               None -> "_"
-             | Some n -> n)) ;
-            Box.b_space; Box.b_text [] ":"; Box.b_space;
-            term2pres ty] in
+        Box.b_hv [Some "helm", "xref", dec_id] 
+          [ Box.b_h []
+            [ Box.b_object (p_mi []
+               (match dec_name with
+                  None -> "_"
+               | Some n -> n)) ;
+              Box.b_space; Box.b_text [] ":"; ];
+             Box.indent (term2pres ty)] in
       aux (r::accum) tl
   | (Some (`Definition d))::tl ->
       let