| C.Meta (i, l), t -> (
try
let _, _, ty = CicUtil.lookup_meta i menv in
- assert (not (Subst.is_in_subst i subst));
let subst = Subst.buildsubst i context t ty subst in
- let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *)
subst, menv
with CicUtil.Meta_not_found m ->
let names = names_of_context context in