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 /.merlin | |
| 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 '.merlin')
| -rw-r--r-- | .merlin | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -1,4 +1,4 @@ -FLG -rectypes -thread +FLG -rectypes -thread -safe-string S ltac B ltac |