Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: himsg.mli Sprache: SML

Original von: Coq^©

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Environ
open Type_errors
open Pretype_errors
open Typeclasses_errors
open Indrec
open Cases
open Logic

(** This module provides functions to explain the type errors. *)

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

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

val explain_inductive_error : inductive_error -> Pp.t

val explain_mismatched_contexts : env -> contexts -> Constrexpr.constr_expr list -> Constr.rel_context -> Pp.t

val explain_typeclass_error : env -> Evd.evar_map -> typeclass_error -> Pp.t

val explain_recursion_scheme_error : env -> recursion_scheme_error -> Pp.t

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

val explain_pattern_matching_error :
  env -> Evd.evar_map -> 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 pguard_error -> 'd pguard_error
[@@ocaml.deprecated "Use [Type_errors.map_pguard_error]."]
val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error
[@@ocaml.deprecated "Use [Type_errors.map_ptype_error]."]

val explain_prim_token_notation_error : string -> env -> Evd.evar_map -> Notation.prim_token_notation_error -> Pp.t

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.