"Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted."
(*
(sprintf
"Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted."
- (CicMetaSubst.ppterm subst t1)
- (CicMetaSubst.ppterm subst t2))) *)
+ (CicMetaSubst.ppterm ~metasenv subst t1)
+ (CicMetaSubst.ppterm ~metasenv subst t2))) *)
| Invalid_argument _ ->
raise
(UnificationFailure (lazy "2")))
(*
(sprintf
"Error trying to unify %s with %s: the lengths of the two local contexts do not match."
| Invalid_argument _ ->
raise
(UnificationFailure (lazy "2")))
(*
(sprintf
"Error trying to unify %s with %s: the lengths of the two local contexts do not match."