From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 3 Apr 2006 13:12:21 +0000 (+0000)
Subject: Useless code simplified out.
X-Git-Tag: make_still_working~7438
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e1676c7a2d2199102d6c6be22b6c248ce4e12860;hp=7429650a9e29e00a78bfd46f2c5a48777e684510;p=helm.git

Useless code simplified out.
---

diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml
index de3bf61f4..ce8f66deb 100644
--- a/helm/software/components/cic_proof_checking/cicReduction.ml
+++ b/helm/software/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 =