From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 15 Apr 2008 08:53:01 +0000 (+0000)
Subject: positivity check fixed, a MutInd not applied (but with an exp-named-subst)
X-Git-Tag: make_still_working~5337
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c59d5065faea77ce41431e273a3331f4d152fbfa;p=helm.git

positivity check fixed, a MutInd not applied (but with an exp-named-subst)
was considere non strictly positive always
---

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