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 /tools/coq_makefile.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 'tools/coq_makefile.ml')
| -rw-r--r-- | tools/coq_makefile.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 23479aee5..4dfb7af6a 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -521,10 +521,10 @@ let variables is_install opt (args,defs) = List.iter (fun c -> print " \\ -I \"$(COQLIB)/"; print c; print "\"") Coq_config.plugins_dirs; print "\n"; print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n\n"; - print "CAMLC?=$(OCAMLFIND) ocamlc -c -rectypes -thread\n"; - print "CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread\n"; - print "CAMLLINK?=$(OCAMLFIND) ocamlc -rectypes -thread\n"; - print "CAMLOPTLINK?=$(OCAMLFIND) opt -rectypes -thread\n"; + print "CAMLC?=$(OCAMLFIND) ocamlc -c -rectypes -thread -safe-string\n"; + print "CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread -safe-string\n"; + print "CAMLLINK?=$(OCAMLFIND) ocamlc -rectypes -thread -safe-string\n"; + print "CAMLOPTLINK?=$(OCAMLFIND) opt -rectypes -thread -safe-string\n"; print "CAMLDEP?=$(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack\n"; print "CAMLLIB?=$(shell $(OCAMLFIND) printconf stdlib)\n"; print "GRAMMARS?=grammar.cma\n"; @@ -764,9 +764,9 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other begin print "mlihtml: $(MLIFILES:.mli=.cmi)\n"; print "\t mkdir $@ || rm -rf $@/*\n"; - print "\t$(OCAMLFIND) ocamldoc -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n"; + print "\t$(OCAMLFIND) ocamldoc -html -safe-string -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n"; print "all-mli.tex: $(MLIFILES:.mli=.cmi)\n"; - print "\t$(OCAMLFIND) ocamldoc -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n"; + print "\t$(OCAMLFIND) ocamldoc -latex -safe-string -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n"; end; if !some_vfile then begin @@ -882,7 +882,7 @@ let check_overlapping_include (_,inc_i,inc_r) = *) let merlin targets (ml_inc,_,_) = print ".merlin:\n"; - print "\t@echo 'FLG -rectypes' > .merlin\n" ; + print "\t@echo 'FLG -rectypes -safe-string' > .merlin\n" ; List.iter (fun c -> printf "\t@echo \"B $(COQLIB)%s\" >> .merlin\n" c) lib_dirs ; |