From 7429017b4f3440ee3abc039be1689ae52f4322c2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 14 Apr 2008 10:21:33 +0000 Subject: [PATCH] fixed positivity conditions --- helm/software/components/ng_kernel/nCicTypeChecker.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index a77b293c1..f9f331240 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -429,7 +429,7 @@ let rec weakly_positive ~subst context n nn uri te = | C.Const (Ref.Ref (_,uri',Ref.Ind _)) | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind _)))::_) when NUri.eq uri' uri -> true | C.Prod (name,source,dest) when - does_not_occur ~subst ((name,C.Decl source)::context) 0 n dest -> + does_not_occur ~subst ((name,C.Decl source)::context) 0 1 dest -> (* dummy abstraction, so we behave as in the anonimous case *) strictly_positive ~subst context n nn (subst_inductive_type_with_dummy_mutind () source) && @@ -505,13 +505,15 @@ and are_all_occurrences_positive ~subst context uri indparamsno i n nn te = (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^ NUri.string_of_uri uri))) | C.Prod (name,source,dest) when - does_not_occur ~subst ((name,C.Decl source)::context) 0 n dest -> + does_not_occur ~subst ((name,C.Decl source)::context) 0 1 dest -> strictly_positive ~subst context n nn source && are_all_occurrences_positive ~subst ((name,C.Decl source)::context) uri indparamsno (i+1) (n + 1) (nn + 1) dest | C.Prod (name,source,dest) -> - does_not_occur ~subst context n nn source && + if not (does_not_occur ~subst context n nn source) then + raise (TypeCheckerFailure (lazy ("Non-positive occurrence in "^ + NCicPp.ppterm ~context ~metasenv:[] ~subst te))); are_all_occurrences_positive ~subst ((name,C.Decl source)::context) uri indparamsno (i+1) (n + 1) (nn + 1) dest | _ -> -- 2.39.2