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 136e9ddaee9150c9eb0acd8d16d7dec0c3986476..f3560cc3afe2733757f6fac1694a3c59328f7ec6 100644 (file)
--- 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
         )