package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val explain_type_error : Environ.env -> Evd.evar_map -> Pretype_errors.type_error -> Pp.t
val explain_pretype_error : Environ.env -> Evd.evar_map -> Pretype_errors.pretype_error -> Pp.t
val explain_inductive_error : Indtypes.inductive_error -> Pp.t
val explain_mismatched_contexts : Environ.env -> Typeclasses_errors.contexts -> Constrexpr.constr_expr list -> Constr.rel_context -> Pp.t
val explain_typeclass_error : Environ.env -> Typeclasses_errors.typeclass_error -> Pp.t
val explain_recursion_scheme_error : Indrec.recursion_scheme_error -> Pp.t
val explain_refiner_error : Environ.env -> Evd.evar_map -> Logic.refiner_error -> Pp.t
val explain_pattern_matching_error : Environ.env -> Evd.evar_map -> Cases.pattern_matching_error -> Pp.t
val explain_reduction_tactic_error : Tacred.reduction_tactic_error -> Pp.t
val explain_module_error : Modops.module_typing_error -> Pp.t
val explain_module_internalization_error : Modintern.module_internalization_error -> Pp.t
val map_pguard_error : ('c -> 'd) -> 'c Type_errors.pguard_error -> 'd Type_errors.pguard_error
val map_ptype_error : ('c -> 'd) -> ('c, 'c) Type_errors.ptype_error -> ('d, 'd) Type_errors.ptype_error
val explain_numeral_notation_error : Environ.env -> Evd.evar_map -> Notation.numeral_notation_error -> Pp.t