if t1 = t2 then
subst, metasenv,ugraph
else
- raise (UnificationFailure (lazy "6.2"))
- (* (sprintf
+ raise (UnificationFailure (lazy
+ (sprintf
"Can't unify %s with %s because they are not convertible"
(CicMetaSubst.ppterm subst t1)
- (CicMetaSubst.ppterm subst t2))) *)
+ (CicMetaSubst.ppterm subst t2))))
| (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
let subst,metasenv,beta_expanded,ugraph1 =
beta_expand_many