exp_named_subst1 exp_named_subst2
else
raise (UnificationFailure (sprintf
"Can't unify %s with %s due to different inductive constructors"
(CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
| (C.Implicit _, _) | (_, C.Implicit _) -> assert false
exp_named_subst1 exp_named_subst2
else
raise (UnificationFailure (sprintf
"Can't unify %s with %s due to different inductive constructors"
(CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
| (C.Implicit _, _) | (_, C.Implicit _) -> assert false