From c63d363ae3e92ca53e7ad010d2efbd69a0c6daae Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 30 Jul 2008 22:41:05 +0000 Subject: [PATCH] fixed check, if 0 constructors then no List.nth is allowed --- .../components/cic_proof_checking/cicTypeChecker.ml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index 111d20126..7fed3ddf3 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -1174,14 +1174,17 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i let non_informative,ugraph = if cl_len = 0 then true,ugraph else - is_non_informative ~logger [Some (C.Name name,C.Decl ty)] - paramsno (snd (List.nth cl 0)) ugraph + let b, ug = + is_non_informative ~logger [Some (C.Name name,C.Decl ty)] + paramsno (snd (List.nth cl 0)) ugraph + in + b && + does_not_occur [Some (C.Name name,C.Decl ty)] 0 1 + (debrujin_constructor uri 1 [] (snd (List.nth cl 0))), ug in (* is it a singleton or empty non recursive and non informative definition? *) - non_informative && - does_not_occur [Some (C.Name name,C.Decl ty)] 0 1 - (debrujin_constructor uri 1 [] (snd (List.nth cl 0))), ugraph + non_informative, ugraph else false,ugraph | _ -> -- 2.39.5