let (metasenv', idx) = mk_implicit metasenv subst context in
let irl = identity_relocation_list_for_metavariable context in
metasenv', Cic.Meta (idx, irl)
let (metasenv', idx) = mk_implicit metasenv subst context in
let irl = identity_relocation_list_for_metavariable context in
metasenv', Cic.Meta (idx, irl)
| Cic.Cast (te, ty) ->
let metasenv', ty' = aux metasenv context ty in
let metasenv'', te' = aux metasenv' context te in
| Cic.Cast (te, ty) ->
let metasenv', ty' = aux metasenv context ty in
let metasenv'', te' = aux metasenv' context te in