+ | _, NCic.Meta (i,lc) when List.mem_assoc i subst ->
+ let cic =
+ let _,_,t,_ = NCicUtils.lookup_subst i subst in
+ NCicSubstitution.subst_meta lc t
+ in
+ select status ctx pat cic
| NCic.LetIn (_,t1,s1,b1), NCic.LetIn (n,t2,s2,b2) ->
let status, t = select status ctx t1 t2 in
let status, s = select status ctx s1 s2 in
| NCic.LetIn (_,t1,s1,b1), NCic.LetIn (n,t2,s2,b2) ->
let status, t = select status ctx t1 t2 in
let status, s = select status ctx s1 s2 in
| NCic.Implicit _, t -> status, t
| _,t ->
fail (lazy ("malformed pattern: " ^ NCicPp.ppterm ~metasenv:[]
| NCic.Implicit _, t -> status, t
| _,t ->
fail (lazy ("malformed pattern: " ^ NCicPp.ppterm ~metasenv:[]
in
let status, term = select low_status context path term in
let term = (name, context, term) in
in
let status, term = select low_status context path term in
let term = (name, context, term) in