From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 14 Apr 2008 09:58:24 +0000 (+0000)
Subject: positivity condition was relying on the name declared in abstractions, and
X-Git-Tag: make_still_working~5346
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3c509cb94d5b11385aa8a3061affd102b47c8cbf;p=helm.git

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 d34c82919..ead71900d 100644
--- 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