positivity check fixed, a MutInd not applied (but with an exp-named-subst)

[helm.git] / helm / software / components / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index ab43c3732ee6b1b572bfb66ed486ecd8439e7838..2855367002ef063677589e455b143d5727453ffa 100644 (file)
--- 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) &&
@@ -437,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
@@ -508,14 +505,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
@@ -2003,7 +1994,7 @@ end;
        let (_,ty,_) = List.nth fl i in
         ty,ugraph2
 
- and check_exp_named_subst ~logger ~subst context ugraph =
+ and check_exp_named_subst ~logger ~subst context =
    let rec check_exp_named_subst_aux ~logger esubsts l ugraph =
      match l with
         [] -> ugraph
@@ -2029,7 +2020,7 @@ end;
                 raise (TypeCheckerFailure (lazy "Wrong Explicit Named Substitution"))
                end
    in
-     check_exp_named_subst_aux ~logger [] ugraph 
+     check_exp_named_subst_aux ~logger []
        
  and sort_of_prod ~subst context (name,s) (t1, t2) ugraph =
   let module C = Cic in