package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.20.1.tar.gz
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2

doc/coq-core.lib/CErrors/index.html

Module CErrorsSource

This modules implements basic manipulations of errors for use throughout Coq's code.

Error handling
Sourceval push : exn -> Exninfo.iexn
  • deprecated please use [Exninfo.capture]
Generic errors.

Anomaly is used for system errors and UserError for the user's ones.

Sourceval anomaly : ?loc:Loc.t -> ?info:Exninfo.info -> ?label:string -> Pp.t -> 'a

Raise an anomaly, with an optional location and an optional label identifying the anomaly.

Sourceval is_anomaly : exn -> bool

Check whether a given exception is an anomaly. This is mostly provided for compatibility. Please avoid doing specific tricks with anomalies thanks to it. See rather noncritical below.

Sourceexception UserError of Pp.t

Main error signaling exception. It carries a header plus a pretty printing doc

Sourceval user_err : ?loc:Loc.t -> ?info:Exninfo.info -> Pp.t -> 'a

Main error raising primitive. user_err ?loc pp signals an error pp with optional header and location loc

Sourceexception Timeout

register_handler h registers h as a handler. When an expression is printed with print e, it goes through all registered handles (the most recent first) until a handle deals with it.

Handles signal that they don't deal with some exception by returning None. Raising any other exception is forbidden and will result in an anomaly.

Exceptions that are considered anomalies should not be handled by registered handlers.

Sourceval register_handler : (exn -> Pp.t option) -> unit
Sourceval print : exn -> Pp.t

The standard exception printer

Sourceval iprint : Exninfo.iexn -> Pp.t
Sourceval print_no_report : exn -> Pp.t

Same as print, except that the "Please report" part of an anomaly isn't printed (used in Ltac debugging).

Sourceval iprint_no_report : Exninfo.iexn -> Pp.t
Sourceval noncritical : exn -> bool

"Critical" exceptions, such as anomalies or interruptions should not be caught and ignored by mistake by inner Coq functions by means of doing a "catch-all". They should be handled instead by the compiler layer which is in charge of coordinating the intepretation of Coq vernaculars.

Please, avoid exceptions catch-all! If you must do so, then use the form:

try my_comp ()
with exn when noncritical exn ->
  my_handler

If you need to re-raise the excepction, you must work to preserve the backtrace and other important information:

try my_comp ()
with exn when noncritical exn ->
  let iexn = Exninfo.capture exn in
  ...
  Exninfo.iraise iexn
Sourceval register_additional_error_info : (Exninfo.info -> Pp.t option) -> unit

Register a printer for errors carrying additional information on exceptions. This method is fragile and should be considered deprecated

Sourceval to_result : f:('a -> 'b) -> 'a -> ('b, Exninfo.iexn) Result.t

to_result ~f x reifies (non-critical) exceptions into a ('a, iexn) Result.t type