diff options
-rw-r--r-- | checker/check.mllib | 1 | ||||
-rw-r--r-- | checker/checker.ml | 7 |
2 files changed, 0 insertions, 8 deletions
diff --git a/checker/check.mllib b/checker/check.mllib index c93051fa1..ea3cb6a8a 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -3,7 +3,6 @@ Pp_control Flags Pp Loc -Compat Segmenttree Unicodetable Unicode diff --git a/checker/checker.ml b/checker/checker.ml index 976030ef5..ea2e3892f 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -231,8 +231,6 @@ let rec explain_exn = function hov 0 (anomaly_string () ++ str "uncaught Stream.Failure.") | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt) - | Compat.Token.Error txt -> - hov 0 (str "Syntax error: " ++ str txt) | Sys_error msg -> hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report() ) | UserError(s,pps) -> @@ -278,11 +276,6 @@ let rec explain_exn = function hov 0 ((if loc = Loc.ghost then (mt ()) else (str"At location " ++ print_loc loc ++ str":" ++ fnl ())) ++ explain_exn exc) - | Compat.Exc_located (loc, exc) -> - let loc = Compat.to_coqloc loc in - hov 0 ((if loc = Loc.ghost then (mt ()) - else (str"At location " ++ print_loc loc ++ str":" ++ fnl ())) - ++ explain_exn exc) | Assert_failure (s,b,e) -> hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++ (if s = "" then mt () |