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:37:23 +0200 |
| commit | a91d15dcb4c691463f0ad6f0e7277a52464d897c (patch) | |
| tree | 6600081af2dc1326b8363e1fd5decda75bd22566 /kernel/nativecode.ml | |
| parent | d90b3c54ea8d26bf6fc48041cb1ca6cba5ba4c19 (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 dabe905de..79e5d3af0 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1486,8 +1486,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 | [] -> "_" @@ -1560,8 +1560,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 |