let old_uninstantiatedmetas,new_uninstantiatedmetas =
(* subst_in doesn't need the context. Hence the underscore. *)
let subst_in _ = CicUnification.apply_subst subst in
- classify_metas newmeta' in_subst_domain subst_in newmetasenv'
+ classify_metas newmeta in_subst_domain subst_in newmetasenv'
in
let bo' =
apply_subst