From aa055bebbc6cd0e99df64020b7f6e26eb19e569a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 3 Nov 2005 15:02:03 +0000 Subject: [PATCH] Semantic change: elimination of a term whose type is defined in a block of mutual inductive empty types --- helm/ocaml/cic_proof_checking/cicTypeChecker.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) 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:" ^ -- 2.39.2