diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-04 16:49:57 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-04 16:49:57 +0000 |
| commit | 88e15b0bd942b4a316afa660da04b6639bccd2dd (patch) | |
| tree | d05e57494d4552649e114c6afc8d9901e0084fba | |
| parent | 41abdd815f9384e197cba73ee67f2b78f89a6319 (diff) | |
Getting rid of Compat in the checker.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15849 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 () |