diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-05-19 20:37:23 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-05-19 20:39:11 +0200 |
| commit | 088b3161c93e46ec2d865fe71a206cee15acd30c (patch) | |
| tree | b3e37912ee49534c0f4a47e79399cbbefc93d18a /kernel/nativecode.ml | |
| parent | 830934afe66f1e6e9314a77a350c3df6c20e4584 (diff) | |
native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)
Diffstat (limited to 'kernel/nativecode.ml')
| -rw-r--r-- | kernel/nativecode.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 9d181b476..2159a702c 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1487,8 +1487,8 @@ let optimize_stk stk = (** Printing to ocaml **) (* Redefine a bunch of functions in module Names to generate names acceptable to OCaml. *) -let string_of_id s = Unicode.ascii_of_ident (string_of_id s) -let string_of_label l = Unicode.ascii_of_ident (string_of_label l) +let string_of_id s = Unicode.ascii_of_ident (Id.to_string s) +let string_of_label l = string_of_id (Label.to_id l) let string_of_dirpath = function | [] -> "_" @@ -1561,8 +1561,7 @@ let pp_gname fmt g = Format.fprintf fmt "%s" (string_of_gname g) let pp_lname fmt ln = - let s = Unicode.ascii_of_ident (string_of_name ln.lname) in - Format.fprintf fmt "x_%s_%i" s ln.luid + Format.fprintf fmt "x_%s_%i" (string_of_name ln.lname) ln.luid let pp_ldecls fmt ids = let len = Array.length ids in |