X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fcontent2pres.ml;h=4d5ec86f5aff02446e9d0b6d44c6278b48991039;hb=2b837ca9e298eb44eee95d9ca0e331c577785dcb;hp=228b6fdeb0cc73c6c08efabc0b618800f6e4976f;hpb=5649890273cf8e660bba744e84ce5fee1e5efe69;p=helm.git

diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index 228b6fdeb..4d5ec86f5 100644
--- a/helm/software/components/content_pres/content2pres.ml
+++ b/helm/software/components/content_pres/content2pres.ml
@@ -183,7 +183,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
         in
         context2pres 
          (match skip_initial_lambdas_internal with
-             Some (`Now n) -> snd (HExtlib.split_nth n p.Con.proof_context)
+             Some (`Now n) -> snd (HExtlib.split_nth "CP 1" n p.Con.proof_context)
            | _ -> p.Con.proof_context)
           presacontext
     in
@@ -815,7 +815,9 @@ let conjecture2pres term2pres (id, n, context, ty) =
   (B.b_hv [Some "helm", "xref", id]
      ((B.b_toggle [
         B.b_h [] [B.b_text [] "{...}"; B.b_space];
-        B.b_hv [] (List.map
+        B.b_hv [] (HExtlib.list_concat ~sep:[B.b_text [] ";"; B.b_space] 
+         (List.map (fun x -> [x])
+         (List.map
           (function
              | None ->
 		 B.b_h []
@@ -833,7 +835,7 @@ let conjecture2pres term2pres (id, n, context, ty) =
 			    (match dec_name with
 				 None -> "_"
 			       | Some n -> n));
-                       B.b_text [] ":";
+                       B.b_text [] ":"; B.b_space; 
                        term2pres ty ]
              | Some (`Definition d) ->
                  let
@@ -846,6 +848,7 @@ let conjecture2pres term2pres (id, n, context, ty) =
 					  None -> "_"
 					| Some n -> n)) ;
                        B.b_text [] (Utf8Macro.unicode_of_tex "\\Assign");
+                       B.b_space;
                        term2pres bo]
              | Some (`Proof p) ->
                  let proof_name = p.Content.proof_name in
@@ -855,12 +858,16 @@ let conjecture2pres term2pres (id, n, context, ty) =
 					  None -> "_"
 					| Some n -> n)) ;
                        B.b_text [] (Utf8Macro.unicode_of_tex "\\Assign");
+                       B.b_space;
                        proof2pres true term2pres p])
-          (List.rev context)) ] ::
+          (List.rev context)))) ] ::
          [ B.b_h []
-           [ B.b_text [] (Utf8Macro.unicode_of_tex "\\vdash");
+           [ B.b_space; 
+             B.b_text [] (Utf8Macro.unicode_of_tex "\\vdash");
+             B.b_space;
              B.b_object (p_mi [] (string_of_int n)) ;
              B.b_text [] ":" ;
+             B.b_space;
              term2pres ty ]])))
 
 let metasenv2pres term2pres = function
@@ -895,8 +902,10 @@ let recursion_kind2pres params kind =
     match kind with
     | `Recursive _ -> "Recursive definition"
     | `CoRecursive -> "CoRecursive definition"
-    | `Inductive _ -> "Inductive definition"
-    | `CoInductive _ -> "CoInductive definition"
+    | `Inductive i -> 
+        "Inductive definition with "^string_of_int i^" fixed parameter(s)"
+    | `CoInductive i -> 
+        "Co-Inductive definition with "^string_of_int i^" fixed parameter(s)"
   in
   B.b_h [] (B.b_kw kind :: params2pres params)