diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-03-09 09:52:04 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-03-09 09:52:04 +0000 |
| commit | 8a64451e6f474d20a469b939a938577bbe6d3d66 (patch) | |
| tree | e49a52973b9fbf726ba2ceff3e7af0ee2b84e617 /driver | |
| parent | 8a26cc219f8c8211301f021bd0ee4a27153528f8 (diff) | |
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
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Driver.ml | 9 |
1 files changed, 9 insertions, 0 deletions
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' |