type_of_aux' metasenv' subst'' context t
in
fo_unif_subst subst'' context metasenv' (S.lift_meta l meta_type) tyt
- with _ ->
+ with AssertFailure _ ->
(* TODO huge hack!!!!
* we keep on unifying/refining in the hope that the problem will be
* eventually solved. In the meantime we're breaking a big invariant: