From 190c0efe22d097c4b4e85207342224622b1fccb9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 30 Jul 2008 15:19:04 +0000 Subject: [PATCH] allowed sort elim now check for recursive types --- helm/software/components/cic_proof_checking/cicTypeChecker.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index fa24119b3..111d20126 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -1179,7 +1179,9 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i in (* is it a singleton or empty non recursive and non informative definition? *) - non_informative, ugraph + non_informative && + does_not_occur [Some (C.Name name,C.Decl ty)] 0 1 + (debrujin_constructor uri 1 [] (snd (List.nth cl 0))), ugraph else false,ugraph | _ -> -- 2.39.2