From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 8 Jul 2009 02:23:02 +0000 (+0000)
Subject: weakly/strictly positive checks relaxed to allow metavariables that are not
X-Git-Tag: make_still_working~3738
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0ef9250d71eacd6b1022194128e6acfb74d52aac;p=helm.git

weakly/strictly positive checks relaxed to allow metavariables that are not
substituted
---

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index c4c2af477..87093e945 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -270,6 +270,12 @@ let rec weakly_positive ~subst context n nn uri indparamsno posuri te =
   let rec aux context n nn te =
     match R.whd ~subst context te with
      | t when t = dummy -> true
+     | C.Meta (i,lc) ->
+        (try
+          let _,_,term,_ = U.lookup_subst i subst in
+          let t = S.subst_meta lc term in
+           weakly_positive ~subst context n nn uri indparamsno posuri t
+         with U.Subst_not_found _ -> true)
      | C.Appl (te::rargs) when te = dummy ->
         List.for_all (does_not_occur ~subst context n nn) rargs
      | C.Prod (name,source,dest) when
@@ -288,6 +294,12 @@ let rec weakly_positive ~subst context n nn uri indparamsno posuri te =
 and strictly_positive ~subst context n nn indparamsno posuri te =
   match R.whd ~subst context te with
    | t when does_not_occur ~subst context n nn t -> true
+   | C.Meta (i,lc) ->
+      (try
+        let _,_,term,_ = U.lookup_subst i subst in
+        let t = S.subst_meta lc term in
+         strictly_positive ~subst context n nn indparamsno posuri t
+       with U.Subst_not_found _ -> true)
    | C.Rel _ when indparamsno = 0 -> true
    | C.Appl ((C.Rel m)::tl) as reduct when m > n && m <= nn ->
       check_homogeneous_call ~subst context indparamsno n posuri reduct tl;