| Cic.Appl ((Cic.MutInd _|Cic.Meta _)::args) as mty,_ ->
snd (HExtlib.split_nth leftno args), mty
| _ -> assert false
- with CicTypeChecker.TypeCheckerFailure _ -> assert false
+ with CicTypeChecker.TypeCheckerFailure _ ->
+ raise (AssertFailure(lazy "already ill-typed matched term"))
in
let new_outty =
keep_lambdas_and_put_expty context outty expty right_p m (rno+1)