diff options
-rw-r--r-- | .gitignore | 2 | ||||
-rw-r--r-- | .typerex | 1 | ||||
-rw-r--r-- | Makefile | 2 | ||||
-rw-r--r-- | Makefile.build | 2 | ||||
-rw-r--r-- | Makefile.common | 6 | ||||
-rw-r--r-- | _tags | 6 | ||||
-rw-r--r-- | myocamlbuild.ml | 6 | ||||
-rw-r--r-- | tools/coqc.ml (renamed from scripts/coqc.ml) | 0 | ||||
-rw-r--r-- | tools/coqmktop.ml (renamed from scripts/coqmktop.ml) | 0 |
9 files changed, 11 insertions, 14 deletions
diff --git a/.gitignore b/.gitignore index 8418d9346..8f0a9a409 100644 --- a/.gitignore +++ b/.gitignore @@ -145,7 +145,7 @@ ide/coqide_main_opt.ml kernel/byterun/coq_jumptbl.h kernel/copcodes.ml -scripts/tolink.ml +tools/tolink.ml theories/Numbers/Natural/BigN/NMake_gen.v ide/index_urls.txt @@ -9,7 +9,6 @@ library plugins pretyping proofs -scripts states tactics theories @@ -78,7 +78,7 @@ EXISTINGMLI := $(call find, '*.mli') GENML4FILES:= $(ML4FILES:.ml4=.ml) GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \ - scripts/tolink.ml kernel/copcodes.ml + tools/tolink.ml kernel/copcodes.ml GENMLIFILES:=$(YACCFILES:.mly=.mli) GENPLUGINSMOD:=$(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml)) export GENHFILES:=kernel/byterun/coq_jumptbl.h diff --git a/Makefile.build b/Makefile.build index 6c2435702..b42432d48 100644 --- a/Makefile.build +++ b/Makefile.build @@ -254,7 +254,7 @@ $(COQMKTOP): $(patsubst %.cma,%$(BESTLIB),$(COQMKTOPCMO:.cmo=$(BESTOBJ))) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD)) -scripts/tolink.ml: Makefile.build Makefile.common +tools/tolink.ml: Makefile.build Makefile.common $(SHOW)"ECHO... >" $@ $(HIDE)echo "let copts = \"-cclib -lcoqrun\"" > $@ $(HIDE)echo "let core_libs = \""$(LINKCMO)"\"" >> $@ diff --git a/Makefile.common b/Makefile.common index 63834dcb0..1934fd493 100644 --- a/Makefile.common +++ b/Makefile.common @@ -72,7 +72,7 @@ PLUGINS:=\ SRCDIRS:=\ $(CORESRCDIRS) \ - tools tools/coqdoc scripts \ + tools tools/coqdoc \ $(addprefix plugins/, $(PLUGINS)) IDESRCDIRS:=\ @@ -224,9 +224,9 @@ IDEMOD:=$(shell cat ide/ide.mllib) COQENVCMO:=lib/clib.cma lib/loc.cmo lib/errors.cmo -COQMKTOPCMO:=$(COQENVCMO) scripts/tolink.cmo scripts/coqmktop.cmo +COQMKTOPCMO:=$(COQENVCMO) tools/tolink.cmo tools/coqmktop.cmo -COQCCMO:=$(COQENVCMO) toplevel/usage.cmo scripts/coqc.cmo +COQCCMO:=$(COQENVCMO) toplevel/usage.cmo tools/coqc.cmo ## Misc @@ -1,8 +1,8 @@ ## tags for binaries -<scripts/coqmktop.{native,byte}> : use_str, use_unix -<scripts/coqc.{native,byte}> : use_str, use_unix +<tools/coqmktop.{native,byte}> : use_str, use_unix +<tools/coqc.{native,byte}> : use_str, use_unix <tools/coqdep_boot.{native,byte}> : use_unix <tools/coqdep.{native,byte}> : use_str, use_unix <tools/coq_tex.{native,byte}> : use_str @@ -68,8 +68,6 @@ "pretyping": include "printing": include "proofs": include -"scripts": include -"states": include "tactics": include "theories": include "tools": include diff --git a/myocamlbuild.ml b/myocamlbuild.ml index f869b4ca7..a0e2e7ef7 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -111,7 +111,7 @@ let core_cma = List.map (fun s -> s^".cma") core_libs let core_cmxa = List.map (fun s -> s^".cmxa") core_libs let core_mllib = List.map (fun s -> s^".mllib") core_libs -let tolink = "scripts/tolink.ml" +let tolink = "tools/tolink.ml" let c_headers_base = ["coq_fix_code.h";"coq_instruct.h"; "coq_memory.h"; "int64_emul.h"; @@ -155,7 +155,7 @@ let coqdepdeps = theoriesv @ pluginsv @ pluginsmllib let coqtop = "toplevel/coqtop" let coqide = "ide/coqide" let coqdepboot = "tools/coqdep_boot" -let coqmktop = "scripts/coqmktop" +let coqmktop = "tools/coqmktop" (** The list of binaries to build: (name of link in bin/, name in _build, install both or only best) *) @@ -167,7 +167,7 @@ let all_binaries = [ "coqtop", coqtop, Both; "coqide", "ide/coqide_main", Ide; "coqmktop", coqmktop, Both; - "coqc", "scripts/coqc", Both; + "coqc", "tools/coqc", Both; "coqchk", "checker/main", Both; "coqdep_boot", coqdepboot, Best; "coqdep", "tools/coqdep", Best; diff --git a/scripts/coqc.ml b/tools/coqc.ml index e15a1768c..e15a1768c 100644 --- a/scripts/coqc.ml +++ b/tools/coqc.ml diff --git a/scripts/coqmktop.ml b/tools/coqmktop.ml index 81f0686e0..81f0686e0 100644 --- a/scripts/coqmktop.ml +++ b/tools/coqmktop.ml |