From 8a64451e6f474d20a469b939a938577bbe6d3d66 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 9 Mar 2012 09:52:04 +0000
Subject: Merge of Andrew Tolmach's HASP-related changes

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1838 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 driver/Driver.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'driver')

diff --git a/driver/Driver.ml b/driver/Driver.ml
index 1ca915c..0523feb 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -35,10 +35,19 @@ let safe_remove file =
 
 (* Printing of error messages *)
 
+(* Locally named idents are encoded as in Cminorgen.
+   This function should live somewhere more central. *)
+let ident_name id =
+   match id with
+  | BinPos.Coq_xO n -> Camlcoq.extern_atom n
+  | BinPos.Coq_xI n -> Printf.sprintf "$%ld" (Camlcoq.camlint_of_positive n)
+  | BinPos.Coq_xH -> "$0"
+
 let print_error oc msg =
   let print_one_error = function
   | Errors.MSG s -> output_string oc (Camlcoq.camlstring_of_coqstring s)
   | Errors.CTX i -> output_string oc (Camlcoq.extern_atom i)
+  | Errors.CTXL i -> output_string oc (ident_name i)
   in
     List.iter print_one_error msg;
     output_char oc '\n'
-- 
cgit v1.2.3