From: Claudio Sacerdoti Coen Date: Thu, 25 Oct 2007 16:35:32 +0000 (+0000) Subject: Bug fixed: a MutCase with missing or exceeding cases was not detected! X-Git-Tag: make_still_working~5951 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4f3c06e2bf0cde557d8d2d3d59b4ed785741cf76;p=helm.git Bug fixed: a MutCase with missing or exceeding cases was not detected! --- diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index b57ad4e78..87a0ca054 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -1814,21 +1814,28 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = in if not b then raise - (TypeCheckerFailure (lazy ("Case analasys: sort elimination not allowed"))); + (TypeCheckerFailure (lazy ("Case analysis: sort elimination not allowed"))); (* let's check if the type of branches are right *) - let parsno = + let parsno,constructorsno = let obj,_ = try CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri with Not_found -> assert false in match obj with - C.InductiveDefinition (_,_,parsno,_) -> parsno + C.InductiveDefinition (il,_,parsno,_) -> + let _,_,_,cl = + try List.nth il i with Failure _ -> assert false + in + parsno, List.length cl | _ -> raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri))) - in + in + if List.length pl <> constructorsno then + raise (TypeCheckerFailure + (lazy ("Wrong number of cases in case analysis"))) ; let (_,branches_ok,ugraph5) = List.fold_left (fun (j,b,ugraph) p ->