From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 3 Nov 2005 15:02:03 +0000 (+0000)
Subject: Semantic change: elimination of a term whose type is defined in a block of
X-Git-Tag: V_0_7_2_3~145
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=aa055bebbc6cd0e99df64020b7f6e26eb19e569a;p=helm.git

Semantic change: elimination of a term whose type is defined in a block of
mutual inductive empty types
---

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 6678d509c..611585400 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1315,11 +1315,16 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
                is_non_informative ~logger [Some (C.Name name,C.Decl ty)]
                 paramsno (snd (List.nth cl 0)) ugraph
              in
-              (* is a singleton or empty non recursive and non informative
+              (* is it a singleton or empty non recursive and non informative
                  definition? *)
               non_informative, ugraph
             else
-             false,ugraph
+             let is_empty =
+              List.fold_left
+               (fun b (_,_,_,cl) -> b && List.length cl = 0) true itl
+             in
+              (* is it a block of mutual inductive empty definitions? *)
+              is_empty,ugraph
          | _ ->
              raise (TypeCheckerFailure 
 		     (lazy ("Unknown mutual inductive definition:" ^