package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

Module `Himsg`Source

This module provides functions to explain the type errors.

val explain_type_error : 
  Environ.env ->
  Evd.evar_map ->
  Pretype_errors.type_error ->
  Pp.t

Source

val explain_pretype_error : 
  Environ.env ->
  Evd.evar_map ->
  Pretype_errors.pretype_error ->
  Pp.t

Source

val explain_refiner_error : 
  Environ.env ->
  Evd.evar_map ->
  Logic.refiner_error ->
  Pp.t

Source

val explain_not_guarded : 
  Environ.env ->
  Evd.evar_map ->
  (Environ.env * int * EConstr.t Type_errors.pcofix_guard_error) option ->
  (Environ.env * int * int list * EConstr.t Type_errors.pfix_guard_error) list ->
  EConstr.rec_declaration ->
  Pp.t

package rocq-runtime

Module HimsgSource

Module `Himsg`Source