diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-12-06 17:16:16 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-21 15:47:14 +0100 |
| commit | f0341076aa60a84177a6b46db0d8d50df220536b (patch) | |
| tree | 3dd3acd080d858e7b4d14ea31231b09c8ec74ec5 /library/libobject.ml | |
| parent | eb68e001f2ebbf09dc32c999e9c9b0f116c0a530 (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 'library/libobject.ml')
| -rw-r--r-- | library/libobject.ml | 12 |
1 files changed, 2 insertions, 10 deletions
diff --git a/library/libobject.ml b/library/libobject.ml index caa03c85b..8757ca08c 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -91,16 +91,8 @@ let declare_object_full odecl = dyn_rebuild_function = rebuild }; (infun,outfun) -(* The "try .. with .. " allows for correct printing when calling - declare_object a loading time. -*) - -let declare_object odecl = - try fst (declare_object_full odecl) - with e -> CErrors.fatal_error (CErrors.print e) (CErrors.is_anomaly e) -let declare_object_full odecl = - try declare_object_full odecl - with e -> CErrors.fatal_error (CErrors.print e) (CErrors.is_anomaly e) +let declare_object odecl = fst (declare_object_full odecl) +let declare_object_full odecl = declare_object_full odecl (* this function describes how the cache, load, open, and export functions are triggered. *) |