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 /lib/loc.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 'lib/loc.ml')
0 files changed, 0 insertions, 0 deletions