From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 21 May 2008 12:23:53 +0000 (+0000)
Subject: minimal implementation of left parameters display
X-Git-Tag: make_still_working~5136
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e8afeae67f66a15433df81e30556276a743b6e05;p=helm.git

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 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)