X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicPp.ml;h=f3560cc3afe2733757f6fac1694a3c59328f7ec6;hb=5cda0ce4c05ede99ad05312d5c9da047978a6898;hp=136e9ddaee9150c9eb0acd8d16d7dec0c3986476;hpb=8b9d2632ab7edc7102d16f3857fde02139cef5c2;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicPp.ml b/helm/software/components/cic_proof_checking/cicPp.ml
index 136e9ddae..f3560cc3a 100644
--- a/helm/software/components/cic_proof_checking/cicPp.ml
+++ b/helm/software/components/cic_proof_checking/cicPp.ml
@@ -139,18 +139,20 @@ let rec pp t l =
     | C.MutCase (uri,n1,ty,te,patterns) ->
        let connames_and_argsno =
         (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
-            C.InductiveDefinition (dl,_,_,_) ->
+            C.InductiveDefinition (dl,_,paramsno,_) ->
              let (_,_,_,cons) = get_nth dl (n1+1) in
               List.map
                (fun id,ty ->
                  (* this is just an approximation since we do not have
                     reduction yet! *)
-                 let rec count_prods =
+                 let rec count_prods toskip =
                   function
-                     C.Prod (_,_,bo) -> 1 + count_prods bo
+                     C.Prod (_,_,bo) when toskip > 0 ->
+                      count_prods (toskip - 1) bo
+                   | C.Prod (_,_,bo) -> 1 + count_prods 0 bo
                    | _ -> 0
                  in
-                  id, count_prods ty
+                  id, count_prods paramsno ty
                ) cons
           | _ -> raise CicPpInternalError
         )