raise (UnificationFailure (sprintf
"Can't unify %s with %s due to different inductive constructors"
(CicPp.ppterm t1) (CicPp.ppterm t1)))
- | (C.Implicit, _) | (_, C.Implicit) -> assert false
+ | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
| (C.Cast (te,ty), t2) -> fo_unif_subst subst context metasenv te t2
| (t1, C.Cast (te,ty)) -> fo_unif_subst subst context metasenv t1 te
| (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->