- | (C.Sort _ ,_) | (_, C.Sort _)
- | (C.Const _, _) | (_, C.Const _)
- | (C.MutInd _, _) | (_, C.MutInd _)
- | (C.MutConstruct _, _) | (_, C.MutConstruct _)
- | (C.Fix _, _) | (_, C.Fix _)
- | (C.CoFix _, _) | (_, C.CoFix _) ->
- if t1 = t2 then
- subst, metasenv, ugraph
- else
- let b,ugraph1 =
- R.are_convertible ~subst ~metasenv context t1 t2 ugraph
- in
- if b then
- subst, metasenv, ugraph1
- else
- raise
- (UnificationFailure (lazy (sprintf
- "Can't unify %s with %s because they are not convertible"
- (CicMetaSubst.ppterm subst t1)
- (CicMetaSubst.ppterm subst t2))))