From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 14 Sep 2006 10:23:29 +0000 (+0000)
Subject: Bug fixed in pretty printing in new syntax of MutCases on inductive types
X-Git-Tag: make_still_working~6895
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7bbe9c8a9fcc471920c18a12fb5745828f2fd188;p=helm.git

Bug fixed in pretty printing in new syntax of MutCases on inductive types
with left parameters.
---

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
         )