From 0ef9250d71eacd6b1022194128e6acfb74d52aac Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 8 Jul 2009 02:23:02 +0000 Subject: [PATCH] weakly/strictly positive checks relaxed to allow metavariables that are not substituted --- .../software/components/ng_kernel/nCicTypeChecker.ml | 12 ++++++++++++ 1 file changed, 12 insertions(+) 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; -- 2.39.2