From f32d668005b27b2eb8cc984a5dd57506b2d1f7e7 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 3 Nov 2005 15:07:55 +0000
Subject: [PATCH] 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.
---
helm/ocaml/cic_proof_checking/cicTypeChecker.ml | 9 ++-------
helm/ocaml/cic_proof_checking/doc/inductive.txt | 5 +++--
2 files changed, 5 insertions(+), 9 deletions(-)
diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 611585400..af98ff0ef 100644
--- 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 4cc9cade6..f2e49d398 100644
--- 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)
--
2.39.5