+let enrich_msg msg subst context metasenv t1 t2 ugraph =
+ lazy (
+ if verbose then
+ sprintf "[Verbose] Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nand substitution\n%s\nbecause %s"
+ (CicMetaSubst.ppterm subst t1)
+ (try
+ let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
+ CicPp.ppterm ty_t1
+ with
+ | UnificationFailure s
+ | Uncertain s
+ | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
+ (CicMetaSubst.ppterm subst t2)
+ (try
+ let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
+ CicPp.ppterm ty_t2
+ 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))
+ (CicMetaSubst.ppcontext subst context)
+ (CicMetaSubst.ppmetasenv subst metasenv)
+ (Lazy.force msg)
+ )
+