| (C.Sort _ ,_)
| (_, C.Sort _)
| (C.Implicit, _)
- | (_, C.Implicit) -> if R.are_convertible t1 t2 then subst
+ | (_, C.Implicit) -> if R.are_convertible context t1 t2 then subst
else raise UnificationFailed
| (C.Cast (te,ty), t2) -> fo_unif_aux subst k te t2
| (t1, C.Cast (te,ty)) -> fo_unif_aux subst k t1 te
| (C.MutInd _, _)
| (_, C.MutInd _)
| (C.MutConstruct _, _)
- | (_, C.MutConstruct _) -> if R.are_convertible t1 t2 then subst
+ | (_, C.MutConstruct _) -> if R.are_convertible context t1 t2 then subst
else raise UnificationFailed
| (C.MutCase (_,_,_,outt1,t1,pl1), C.MutCase (_,_,_,outt2,t2,pl2))->
let subst' = fo_unif_aux subst k outt1 outt2 in
| (C.Fix _, _)
| (_, C.Fix _)
| (C.CoFix _, _)
- | (_, C.CoFix _) -> if R.are_convertible t1 t2 then subst
+ | (_, C.CoFix _) -> if R.are_convertible context t1 t2 then subst
else raise UnificationFailed
| (_,_) -> raise UnificationFailed
in fo_unif_aux [] 0 t1 t2;;