From 88e15b0bd942b4a316afa660da04b6639bccd2dd Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Thu, 4 Oct 2012 16:49:57 +0000
Subject: 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
---
 checker/check.mllib | 1 -
 checker/checker.ml  | 7 -------
 2 files changed, 8 deletions(-)

diff --git a/checker/check.mllib b/checker/check.mllib
index c93051fa18..ea3cb6a8a3 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 976030ef5d..ea2e3892f0 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 ()
-- 
cgit v1.2.3