X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_proof_checking%2FcicReduction.ml;h=ce8f66deb04aa554763f84ecf26299622aed11ac;hb=25835a1eac5698fedca50ebae1e18bef49a67c87;hp=de3bf61f4dd6e5a8092cca6466476023e99cbb14;hpb=afc19735fc5b88c8e841d6e62e58f21a81f06d8c;p=helm.git

diff --git a/components/cic_proof_checking/cicReduction.ml b/components/cic_proof_checking/cicReduction.ml
index de3bf61f4..ce8f66deb 100644
--- a/components/cic_proof_checking/cicReduction.ml
+++ b/components/cic_proof_checking/cicReduction.ml
@@ -664,14 +664,12 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
              (k', e', ens', C.MutConstruct (_,_,j,_), []) ->
               reduce (k, e, ens, (List.nth pl (j-1)), s)
            | (k', e', ens', C.MutConstruct (_,_,j,_), s') ->
-              let (arity, r) =
+              let r =
                 let o,_ = 
                   CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind 
                 in
                   match o with
-                      C.InductiveDefinition (s,ingredients,r,_) ->
-                        let (_,_,arity,_) = List.nth s i in
-                          (arity,r)
+                      C.InductiveDefinition (_,_,r,_) -> r
                     | _ -> raise WrongUriToInductiveDefinition
               in
                let ts =