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 6678d509cbcb9ad15f33c7e5e1f0b64be3d6f2b4..611585400c69251e86d8b34b5ee8a67b1121e70d 100644 (file)
--- 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:" ^