minimal implementation of left parameters display

diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index 228b6fdeb0cc73c6c08efabc0b618800f6e4976f..f7b7067cc0a90649db11182b5c83bb6c79fec02f 100644 (file)
--- 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)