positivity condition was relying on the name declared in abstractions, and

was checking for a dependent product calling does not occurr with a wrong
index

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index d34c829199e506cf1925c46402104b9e43295a20..ead71900d7a1c3c3f4f666e4701077e1a8cddbb1 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) &&
@@ -508,14 +503,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