Module Himsg
This module provides functions to explain the type errors.
val explain_type_error : Environ.env -> Evd.evar_map -> Pretype_errors.type_error -> Pp.tval explain_pretype_error : Environ.env -> Evd.evar_map -> Pretype_errors.pretype_error -> Pp.tval explain_inductive_error : Type_errors.inductive_error -> Pp.tval explain_mismatched_contexts : Environ.env -> Typeclasses_errors.contexts -> Constrexpr.constr_expr list -> Constr.rel_context -> Pp.tval explain_typeclass_error : Environ.env -> Evd.evar_map -> Typeclasses_errors.typeclass_error -> Pp.tval explain_recursion_scheme_error : Environ.env -> Indrec.recursion_scheme_error -> Pp.tval explain_refiner_error : Environ.env -> Evd.evar_map -> Logic.refiner_error -> Pp.tval explain_pattern_matching_error : Environ.env -> Evd.evar_map -> Cases.pattern_matching_error -> Pp.tval explain_reduction_tactic_error : Tacred.reduction_tactic_error -> Pp.tval explain_module_error : Modops.module_typing_error -> Pp.tval explain_module_internalization_error : Modintern.module_internalization_error -> Pp.tval map_pguard_error : ('c -> 'd) -> 'c Type_errors.pguard_error -> 'd Type_errors.pguard_errorval map_ptype_error : ('c -> 'd) -> ('c, 'c) Type_errors.ptype_error -> ('d, 'd) Type_errors.ptype_errorval explain_prim_token_notation_error : string -> Environ.env -> Evd.evar_map -> Notation.prim_token_notation_error -> Pp.t