From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
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 ->