else
raise (UnificationFailure (sprintf
"Can't unify %s with %s due to different constants"
- (CicPp.ppterm t1) (CicPp.ppterm t1)))
+ (CicPp.ppterm t1) (CicPp.ppterm t2)))
| C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
if UriManager.eq uri1 uri2 && i1 = i2 then
fo_unif_subst_exp_named_subst subst context metasenv