- if b then
- candidate_oty,ugraph1,metasenv
- else
- None,ugraph,metasenv
- with Failure s -> None,ugraph,metasenv
- ) (Some instance',ugraph4,metasenv) tl
+ candidate_oty,ugraph,metasenv,subst
+ with
+ CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ ->
+ None,ugraph,metasenv,subst
+ ) (Some instance',ugraph4,metasenv,subst) tl