From 5b6582f8d47975f6f4f394cf44a1c65c799d43ff Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Thu, 4 Oct 2012 11:53:07 +0000
Subject: Moved Compat to parsing. This permits to break the dependency of the
 kernel on CAMLP4/5 structures, and consequently should also erase such
 structures from vo files.

This modification requires some code duplication, mainly while
reimplementing our own location data type. This is chiefly visible
in the ml4 files, where CAMLP4/5 locations must be manually converted
to our locations with an explicit (!@) cast operator.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15847 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 checker/check.mllib | 2 +-
 checker/checker.ml  | 7 ++++++-
 2 files changed, 7 insertions(+), 2 deletions(-)

(limited to 'checker')

diff --git a/checker/check.mllib b/checker/check.mllib
index c12b5953a1..c93051fa18 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -1,9 +1,9 @@
 Coq_config
 Pp_control
-Compat
 Flags
 Pp
 Loc
+Compat
 Segmenttree
 Unicodetable
 Unicode
diff --git a/checker/checker.ml b/checker/checker.ml
index a75aed5332..976030ef5d 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -274,7 +274,12 @@ let rec explain_exn = function
 (*      let ctx = Check.get_env() in
       hov 0
         (str "Error:" ++ spc () ++ Himsg.explain_inductive_error ctx e)*)
-  | Loc.Exc_located (loc,exc) ->
+  | Loc.Exc_located (loc, exc) ->
+      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)
-- 
cgit v1.2.3