) (subst'',metasenv'',ugraph2) pl1 pl2
with
Invalid_argument _ ->
- raise (UnificationFailure (lazy "6")))
+ raise (UnificationFailure (lazy "6.1")))
(* (sprintf
"Error trying to unify %s with %s: the number of branches is not the same."
(CicMetaSubst.ppterm subst t1)
if t1 = t2 then
subst, metasenv,ugraph
else
- raise (UnificationFailure (lazy "6"))
+ raise (UnificationFailure (lazy "6.2"))
(* (sprintf
"Can't unify %s with %s because they are not convertible"
(CicMetaSubst.ppterm subst t1)