package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.19.2.tar.gz
md5=5d1187d5e44ed0163f76fb12dabf012e
sha512=91bc81530fa4f6498961583ad51eac5001f139881788b88e360a866ad8e2a6e2c5bce86d1a580ab4cd4782bf49d48318767df82471ce33ba3ac143e5569ad33c
doc/coq-core.clib/Exninfo/index.html
Module Exninfo
Source
Additional information worn by exceptions.
Information containing a given type.
All information
Get information worn by an exception. Returns None
if undefined.
get_backtrace info
does get the backtrace associated to info
backtrace_to_string info
does get the backtrace associated to info
Add the current backtrace information and other meta-data to the given exception.
The intended use case is to re-raise an exception while preserving the meta-data:
try foo
with
| Bar -> bar
| My_exn _ as exn ->
let (exn, info) = Exninfo.capture err in
...
let info = ... in
Exninfo.iraise (exn, info)
| exn when CErrors.noncritical exn ->
let iexn = Exninfo.capture err in
...
Exninfo.iraise iexn
where baz
should re-raise using iraise
below.
WARNING: any intermediate code between the with
and the handler may modify the backtrace. Yes, that includes when
clauses. Ideally, what you should do is something like:
try foo
with exn when CErrors.noncritical exn ->
let (err, info) = Exninfo.capture exn in
match err with
| exception Bar -> ...
| err -> ...
I admit that's a bit heavy, but there is not much to do...
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>