+ with
+ | UnificationFailure s
+ | Uncertain s
+ | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
+ (CicMetaSubst.ppcontext subst context)
+ (CicMetaSubst.ppmetasenv subst metasenv)
+ (CicMetaSubst.ppsubst subst) (Lazy.force msg)
+ else
+ sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
+ (CicMetaSubst.ppterm_in_context subst t1 context)
+ (try
+ let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
+ CicMetaSubst.ppterm_in_context subst ty_t1 context
+ with
+ | UnificationFailure s
+ | Uncertain s
+ | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
+ (CicMetaSubst.ppterm_in_context subst t2 context)
+ (try
+ let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
+ CicMetaSubst.ppterm_in_context subst ty_t2 context
+ with
+ | UnificationFailure s
+ | Uncertain s
+ | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))