X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fcontent2pres.ml;fp=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fcontent2pres.ml;h=f7b7067cc0a90649db11182b5c83bb6c79fec02f;hb=e8afeae67f66a15433df81e30556276a743b6e05;hp=228b6fdeb0cc73c6c08efabc0b618800f6e4976f;hpb=2fbef023cc9fdb3d6982194ba62552a0605f2571;p=helm.git

diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index 228b6fdeb..f7b7067cc 100644
--- a/helm/software/components/content_pres/content2pres.ml
+++ b/helm/software/components/content_pres/content2pres.ml
@@ -895,8 +895,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)