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 : Type_errors.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 -> Evd.evar_map -> Typeclasses_errors.typeclass_error -> Pp.t
val explain_recursion_scheme_error : Environ.env -> 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
  • deprecated Use [Type_errors.map_pguard_error].
val map_ptype_error : ('c -> 'd) -> ('c, 'c) Type_errors.ptype_error -> ('d, 'd) Type_errors.ptype_error
  • deprecated Use [Type_errors.map_ptype_error].
val explain_prim_token_notation_error : string -> Environ.env -> Evd.evar_map -> Notation.prim_token_notation_error -> Pp.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct