From 3c509cb94d5b11385aa8a3061affd102b47c8cbf Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 14 Apr 2008 09:58:24 +0000 Subject: [PATCH] positivity condition was relying on the name declared in abstractions, and was checking for a dependent product calling does not occurr with a wrong index --- .../cic_proof_checking/cicTypeChecker.ml | 15 ++------------- 1 file changed, 2 insertions(+), 13 deletions(-) diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index d34c82919..ead71900d 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -391,13 +391,8 @@ and weakly_positive context n nn uri te = *) C.Appl ((C.MutInd (uri',_,_))::tl) when UriManager.eq uri' uri -> true | C.MutInd (uri',0,_) when UriManager.eq uri' uri -> true - | C.Prod (C.Anonymous,source,dest) -> - strictly_positive context n nn - (subst_inductive_type_with_dummy_mutind source) && - weakly_positive ((Some (C.Anonymous,(C.Decl source)))::context) - (n + 1) (nn + 1) uri dest | C.Prod (name,source,dest) when - does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest -> + does_not_occur ((Some (name,(C.Decl source)))::context) 0 1 dest -> (* dummy abstraction, so we behave as in the anonimous case *) strictly_positive context n nn (subst_inductive_type_with_dummy_mutind source) && @@ -508,14 +503,8 @@ and are_all_occurrences_positive context uri indparamsno i n nn te = raise (TypeCheckerFailure (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^ UriManager.string_of_uri uri))) - | C.Prod (C.Anonymous,source,dest) -> - let b = strictly_positive context n nn source in - b && - are_all_occurrences_positive - ((Some (C.Anonymous,(C.Decl source)))::context) uri indparamsno - (i+1) (n + 1) (nn + 1) dest | C.Prod (name,source,dest) when - does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest -> + does_not_occur ((Some (name,(C.Decl source)))::context) 0 1 dest -> (* dummy abstraction, so we behave as in the anonimous case *) strictly_positive context n nn source && are_all_occurrences_positive -- 2.39.2