diff options
Diffstat (limited to 'src/_build/reporting_basic.ml')
| -rw-r--r-- | src/_build/reporting_basic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/_build/reporting_basic.ml b/src/_build/reporting_basic.ml index a0d53ab0..b3880598 100644 --- a/src/_build/reporting_basic.ml +++ b/src/_build/reporting_basic.ml @@ -162,7 +162,7 @@ exception Fatal_error of error let err_todo l m = Fatal_error (Err_todo (l, m)) let err_unreachable l m = Fatal_error (Err_unreachable (l, m)) let err_general l m = Fatal_error (Err_general (l, m)) - +let err_typ l m = Fatal_error (Err_type (l,m)) let report_error e = let (m1, verb_pos, pos_l, m2) = dest_err e in |