| NCic.Meta (i,_) ->
(try
let _,_,t,_ = List.assoc i subst in
| NCic.Meta (i,_) ->
(try
let _,_,t,_ = List.assoc i subst in
with Not_found -> true)
| NCic.Appl (NCic.Meta (i,_) :: args)->
(try
let _,_,t,_ = List.assoc i subst in
with Not_found -> true)
| NCic.Appl (NCic.Meta (i,_) :: args)->
(try
let _,_,t,_ = List.assoc i subst in
match l with
| _, NCic.Irl _ -> fun _ _ _ _ _ -> None
| shift, NCic.Ctx l -> fun metasenv subst context k t ->
match l with
| _, NCic.Irl _ -> fun _ _ _ _ _ -> None
| shift, NCic.Ctx l -> fun metasenv subst context k t ->
lb
in
let rec aux (context,k,in_scope) (metasenv, subst as ms) t =
lb
in
let rec aux (context,k,in_scope) (metasenv, subst as ms) t =