aboutsummaryrefslogtreecommitdiffhomepage
path: root/COMPATIBILITY
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2016-12-06 17:16:16 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-03-21 15:47:14 +0100
commitf0341076aa60a84177a6b46db0d8d50df220536b (patch)
tree3dd3acd080d858e7b4d14ea31231b09c8ec74ec5 /COMPATIBILITY
parenteb68e001f2ebbf09dc32c999e9c9b0f116c0a530 (diff)
[error] Move back fatal_error to toplevel
This reverts 4444768d3f4f9c4fcdd440f7ab902886bd8e2b09 (the mllib dependencies that should be surely tweaked more). The logic for `fatal_error` has no place in `CErrors`, this is coqtop-specific code. What is more, a libobject caller should handle the exception correctly, I fail to see why the fix was needed on the first place.
Diffstat (limited to 'COMPATIBILITY')
0 files changed, 0 insertions, 0 deletions