+ | ProofEngineTypes.Fail msg -> "Tactic error: " ^ Lazy.force msg
+ | Continuationals.Error s -> "Tactical error: " ^ Lazy.force s
+ | CicTypeChecker.TypeCheckerFailure msg ->
+ "Type checking error: " ^ Lazy.force msg
+ | CicTypeChecker.AssertFailure msg ->
+ "Type checking assertion failed: " ^ Lazy.force msg