From 196682332b4b2ef9ef18459b34ac15d4bd51e463 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 25 Oct 2007 16:35:32 +0000 Subject: [PATCH] Bug fixed: a MutCase with missing or exceeding cases was not detected! --- components/cic_proof_checking/cicTypeChecker.ml | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/components/cic_proof_checking/cicTypeChecker.ml b/components/cic_proof_checking/cicTypeChecker.ml index b57ad4e78..87a0ca054 100644 --- a/components/cic_proof_checking/cicTypeChecker.ml +++ b/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 -> -- 2.39.2