package coq-core
Install
Dune Dependency
Authors
Maintainers
Sources
sha512=2f77bcb5211018b5d46320fd39fd34450eeb654aca44551b28bb50a2364398c4b34587630b6558db867ecfb63b246fd3e29dc2375f99967ff62bc002db9c3250
doc/coq-core.lib/CErrors/index.html
Module CErrorsSource
This modules implements basic manipulations of errors for use throughout Coq's code.
Error handling
Generic errors.
Anomaly is used for system errors and UserError for the user's ones.
Raise an anomaly, with an optional location and an optional label identifying the anomaly.
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.
Main error signaling exception. It carries a header plus a pretty printing doc
Main error raising primitive. user_err ?loc pp signals an error pp with optional header and location loc
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.
Same as print, except that the "Please report" part of an anomaly isn't printed (used in Ltac debugging).
Critical exceptions should not be caught and ignored by mistake by inner functions during a vernacinterp. They should be handled only in Toplevel.do_vernac (or Ideslave), to be displayed to the user. Typical example: Sys.Break, Assert_failure, Anomaly ...
Register a printer for errors carrying additional information on exceptions. This method is fragile and should be considered deprecated