aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-10-04 11:53:07 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-10-04 11:53:07 +0000
commit5b6582f8d47975f6f4f394cf44a1c65c799d43ff (patch)
treee1be15920daf8b2e5ae788f57e772e79ddaacd30 /checker
parent621625757d04bdb19075d92e764749d0a1393ce3 (diff)
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
Diffstat (limited to 'checker')
-rw-r--r--checker/check.mllib2
-rw-r--r--checker/checker.ml7
2 files changed, 7 insertions, 2 deletions
diff --git a/checker/check.mllib b/checker/check.mllib
index c12b5953a..c93051fa1 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 a75aed533..976030ef5 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)