fixed positivity conditions

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index a77b293c1ae42d67ef8bdc0bdf09471441d431ef..f9f3312408358fde025b1683cbfdebcd596d75e8 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -429,7 +429,7 @@ let rec weakly_positive ~subst context n nn uri te =
    | C.Const (Ref.Ref (_,uri',Ref.Ind _))
    | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind _)))::_) when NUri.eq uri' uri -> true
    | C.Prod (name,source,dest) when
-      does_not_occur ~subst ((name,C.Decl source)::context) 0 n dest ->
+      does_not_occur ~subst ((name,C.Decl source)::context) 0 1 dest ->
        (* dummy abstraction, so we behave as in the anonimous case *)
        strictly_positive ~subst context n nn
         (subst_inductive_type_with_dummy_mutind () source) &&
@@ -505,13 +505,15 @@ and are_all_occurrences_positive ~subst context uri indparamsno i n nn te =
          (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^
           NUri.string_of_uri uri)))
   | C.Prod (name,source,dest) when
-      does_not_occur ~subst ((name,C.Decl source)::context) 0 n dest ->
+      does_not_occur ~subst ((name,C.Decl source)::context) 0 1 dest ->
       strictly_positive ~subst context n nn source &&
        are_all_occurrences_positive ~subst 
         ((name,C.Decl source)::context) uri indparamsno
         (i+1) (n + 1) (nn + 1) dest
    | C.Prod (name,source,dest) ->
-      does_not_occur ~subst context n nn source &&
+       if not (does_not_occur ~subst context n nn source) then
+         raise (TypeCheckerFailure (lazy ("Non-positive occurrence in "^
+         NCicPp.ppterm ~context ~metasenv:[] ~subst te)));
        are_all_occurrences_positive ~subst ((name,C.Decl source)::context)
         uri indparamsno (i+1) (n + 1) (nn + 1) dest
    | _ ->