From: Claudio Sacerdoti Coen 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:" ^