From c59d5065faea77ce41431e273a3331f4d152fbfa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 15 Apr 2008 08:53:01 +0000 Subject: [PATCH] positivity check fixed, a MutInd not applied (but with an exp-named-subst) was considere non strictly positive always --- 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 ead71900d..285536700 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -432,7 +432,9 @@ and strictly_positive context n nn te = strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) ta | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true - | C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) -> + | C.Appl ((C.MutInd (uri,i,exp_named_subst))::_) + | (C.MutInd (uri,i,exp_named_subst)) as t -> + let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in let (ok,paramsno,ity,cl,name) = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with -- 2.39.2