From 5e2574cbef1ba132aacc73b4a079cc0b5584f589 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 23 Feb 2017 14:57:59 +0100 Subject: [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. --- tools/coq_makefile.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'tools/coq_makefile.ml') 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 ; -- cgit v1.2.3