diff options
| author | Enrico Tassi | 2016-06-16 16:33:17 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2016-06-16 16:36:40 +0200 |
| commit | 8ee9906d70e0181a0e247b3ec0adbe889f3fdbce (patch) | |
| tree | 74f88c5852f096c18b408fc383a0ac2c384f8b01 | |
| parent | a33999800dc7e0a12935034350c31b47b6e5d494 (diff) | |
| parent | fcdd3fe3c327ecac88880165d14f13ff796510f3 (diff) | |
Merge '/pr/206' into trunk
| -rw-r--r-- | toplevel/cerrors.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli index a0e3e3c199..cd6ccd5653 100644 --- a/toplevel/cerrors.mli +++ b/toplevel/cerrors.mli @@ -6,6 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Toplevel Exception *) +exception EvaluatedError of Pp.std_ppcmds * exn option + (** Error report. *) val print_loc : Loc.t -> Pp.std_ppcmds |