From e1676c7a2d2199102d6c6be22b6c248ce4e12860 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 3 Apr 2006 13:12:21 +0000 Subject: [PATCH 1/1] Useless code simplified out. --- helm/software/components/cic_proof_checking/cicReduction.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) 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 = -- 2.39.2