-
-let explain_error =
- function
- Reason msg -> msg
- | Enriched (msg,subst,context,metasenv,t1,t2,ugraph) ->
- sprintf "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 _ -> "MALFORMED")
- (CicMetaSubst.ppterm subst t2)
- (try
- let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
- CicPp.ppterm ty_t2
- with _ -> "MALFORMED")
- (CicMetaSubst.ppcontext subst context)
- (CicMetaSubst.ppmetasenv subst metasenv)
- (CicMetaSubst.ppsubst subst) msg