+ try
+ fo_unif_subst false subst context metasenv t1 t2 ugraph
+ with
+ | AssertFailure (Enriched _ as msg) -> assert false
+ | AssertFailure (Reason msg) ->
+ raise (AssertFailure (Enriched (msg,subst,context,metasenv,t1,t2,ugraph)))
+ | UnificationFailure (Enriched _ as msg) -> assert false
+ | UnificationFailure (Reason msg) ->
+ raise (UnificationFailure (Enriched (msg,subst,context,metasenv,t1,t2,ugraph)))
+;;
+
+let explain_error =
+ function
+ Reason msg -> msg
+ | Enriched (msg,subst,context,metasenv,t1,t2,ugraph) ->