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 ead71900d7a1c3c3f4f666e4701077e1a8cddbb1..2855367002ef063677589e455b143d5727453ffa 100644 (file)
--- 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