diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-02-23 14:57:59 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-14 22:19:27 +0100 |
commit | 5e2574cbef1ba132aacc73b4a079cc0b5584f589 (patch) | |
tree | d1d3fc20d3d9684e82b538c468324c897dfeff1e /kernel/names.ml | |
parent | 92579449f62f0fd7699b0b447f3aee0d82d1b5c3 (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.ml | 4 |
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 |