perform substitution only if DoesOccur is raised *)
let _,_,term,_ = U.lookup_subst mno subst in
aux (k-s) () (S.subst_meta (0,l) term)
- with U.Subst_not_found _ -> match l with
+ with U.Subst_not_found _ -> () (*match l with
| C.Irl len -> if not (n+k >= s+len || s > nn+k) then raise DoesOccur
- | C.Ctx lc -> List.iter (aux (k-s) ()) lc)
+ | C.Ctx lc -> List.iter (aux (k-s) ()) lc*))
| t -> U.fold (fun _ k -> k + 1) k aux () t
in
try aux 0 () t; true
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
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;
with Failure _ ->
raise (TypeCheckerFailure (lazy ("unbound variable " ^ string_of_int n
^" under: " ^ NCicPp.ppcontext ~metasenv ~subst context))))
- | C.Sort (C.Type [false,u]) -> C.Sort (C.Type [true, u])
+ | C.Sort (C.Type ([false,u] as univ)) ->
+ if NCicEnvironment.is_declared univ then
+ C.Sort (C.Type [true, u])
+ else
+ raise (TypeCheckerFailure (lazy ("undeclared universe " ^
+ NUri.string_of_uri u)))
| C.Sort (C.Type _) ->
raise (AssertFailure (lazy ("Cannot type an inferred type: "^
NCicPp.ppterm ~subst ~metasenv ~context t)))