aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/names.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-02-23 14:57:59 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-03-14 22:19:27 +0100
commit5e2574cbef1ba132aacc73b4a079cc0b5584f589 (patch)
treed1d3fc20d3d9684e82b538c468324c897dfeff1e /kernel/names.ml
parent92579449f62f0fd7699b0b447f3aee0d82d1b5c3 (diff)
[safe-string] Enable -safe-string !
We now build Coq with `-safe-string`, which enforces functional use of the `string` datatype. Coq was pretty safe in these regard so only a few tweaks were needed. - coq_makefile: build plugins with -safe-string too. - `names.ml`: we remove `String.copy` uses, as they are not needed.
Diffstat (limited to 'kernel/names.ml')
-rw-r--r--kernel/names.ml4
1 files changed, 1 insertions, 3 deletions
diff --git a/kernel/names.ml b/kernel/names.ml
index 831b6ad46..ee8d838da 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -57,15 +57,13 @@ struct
let of_string s =
let () = check_soft s in
- let s = String.copy s in
String.hcons s
let of_string_soft s =
let () = check_soft ~warn:false s in
- let s = String.copy s in
String.hcons s
- let to_string id = String.copy id
+ let to_string id = id
let print id = str id