From f32d668005b27b2eb8cc984a5dd57506b2d1f7e7 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen 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.2