From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 25 Oct 2007 16:41:20 +0000 (+0000)
Subject: Bug fixed: a MutCase considering a wrong number of cases was not detected.
X-Git-Tag: make_still_working~5950
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5357e090aa81403bd99bb56a023a5d46d34d92f0;p=helm.git

Bug fixed: a MutCase considering a wrong number of cases was not detected.
---

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 4b310ef75..7f5ab6883 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -527,6 +527,10 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                        (lazy ("Unkown mutual inductive definition " ^ 
                          U.string_of_uri uri)))
            in
+           if List.length constructors <> List.length pl then
+            enrich localization_tbl t
+             (RefineFailure
+               (lazy "Wrong number of cases")) ;
            let rec count_prod t =
              match CicReduction.whd ~subst context t with
                  C.Prod (_, _, t) -> 1 + (count_prod t)