(NCicPp.ppterm ~metasenv ~subst ~context he)
(NCicPp.ppterm ~metasenv ~subst ~context t)
(NCicPp.ppterm ~metasenv ~subst ~context arg)
- (NCicPp.ppterm ~metasenv ~subst ~context ty_arg))) exc)
+ (NCicPp.ppterm ~metasenv ~subst ~context ty_arg)))
+ (match exc with
+ | NCicUnification.UnificationFailure m ->
+ NCicUnification.Uncertain m
+ | x -> x))
(* XXX coerce to funclass *)
in
let meta = NCicSubstitution.subst ~avoid_beta_redexes:true arg meta in