From e8afeae67f66a15433df81e30556276a743b6e05 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 21 May 2008 12:23:53 +0000 Subject: [PATCH] minimal implementation of left parameters display --- helm/software/components/content_pres/content2pres.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) 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) -- 2.39.2