Semantic change: I always consider a type with no constructors as an empty

type even if it is mutually recursive with non-empty types. I think that
this should be a sound generalization.

Note: Coq assumes a type to be empty iff it is not mutually recursive with
any other inductive type.

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 611585400c69251e86d8b34b5ee8a67b1121e70d..af98ff0efc72b53acfd7d7e8b225e45272a166f4 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1308,7 +1308,7 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
            let itl_len = List.length itl in
            let (name,_,ty,cl) = List.nth itl i in
            let cl_len = List.length cl in
-            if (itl_len = 1 && cl_len <= 1) then
+            if (cl_len = 0 || (itl_len = 1 && cl_len = 1)) then
              let non_informative,ugraph =
               if cl_len = 0 then true,ugraph
               else
@@ -1319,12 +1319,7 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
                  definition? *)
               non_informative, ugraph
             else
-             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
+              false,ugraph
          | _ ->
              raise (TypeCheckerFailure 
                     (lazy ("Unknown mutual inductive definition:" ^

diff --git a/helm/ocaml/cic_proof_checking/doc/inductive.txt b/helm/ocaml/cic_proof_checking/doc/inductive.txt
index 4cc9cade63223e35908d996a7aa7573dee4d0d41..f2e49d3987fb770d9d3e940dd4094583f41f9aca 100644 (file)
--- a/helm/ocaml/cic_proof_checking/doc/inductive.txt
+++ b/helm/ocaml/cic_proof_checking/doc/inductive.txt
@@ -36,5 +36,6 @@ Legenda:
   non-informative : Constructor arguments are in Prop only
   small : Constructor arguments are not in Type and SetP and CProp
   unit : Non (mutually) recursive /\ only one constructor /\ non-informative
-  empty : no contructors and (in Coq) non mutually recursive
-            
+  empty : in Coq:    no constructors and non mutually recursive
+          in Matita: no constructors (but eventually mutually recursive
+                     with non-empty types)