diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-07-04 16:48:01 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-07-11 01:28:43 +0200 |
| commit | dd25b08c3608b55dd9edb24304168efb56bc64c8 (patch) | |
| tree | 04f7a631e0b223a74958571b99cd7abaac2b1852 | |
| parent | d47ddf56bc93ae16280ce8a845a4b004fef52fb8 (diff) | |
[coqpp] Move to its own directory.
Coqpp has nothing to do with `grammar`, we thus place it in its own
directory, which will prove convenient in more modular build systems.
Note that we add `coqpp` to the list of global includes, we could have
indeed added some extra rules, but IMHO not worth it as hopefully
proper containment will be soon checked by Dune.
| -rw-r--r-- | .gitignore | 6 | ||||
| -rw-r--r-- | Makefile.build | 12 | ||||
| -rw-r--r-- | Makefile.common | 1 | ||||
| -rw-r--r-- | coqpp/coqpp_ast.mli (renamed from grammar/coqpp_ast.mli) | 0 | ||||
| -rw-r--r-- | coqpp/coqpp_lex.mll (renamed from grammar/coqpp_lex.mll) | 0 | ||||
| -rw-r--r-- | coqpp/coqpp_main.ml (renamed from grammar/coqpp_main.ml) | 0 | ||||
| -rw-r--r-- | coqpp/coqpp_parse.mly (renamed from grammar/coqpp_parse.mly) | 0 |
7 files changed, 10 insertions, 9 deletions
diff --git a/.gitignore b/.gitignore index 466f4c1a7..14ec71b93 100644 --- a/.gitignore +++ b/.gitignore @@ -115,7 +115,7 @@ dev/ocamldoc/*.css # .mll files -grammar/coqpp_lex.ml +coqpp/coqpp_lex.ml dev/ocamlweb-doc/lex.ml ide/coq_lex.ml ide/config_lexer.ml @@ -128,8 +128,8 @@ ide/protocol/xml_lexer.ml # .mly files -grammar/coqpp_parse.ml -grammar/coqpp_parse.mli +coqpp/coqpp_parse.ml +coqpp/coqpp_parse.mli # .ml4 / .mlp files diff --git a/Makefile.build b/Makefile.build index 2e14dab54..84f86c99a 100644 --- a/Makefile.build +++ b/Makefile.build @@ -350,7 +350,7 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h GRAMBASEDEPS := grammar/q_util.cmi GRAMCMO := grammar/q_util.cmo \ grammar/argextend.cmo grammar/tacextend.cmo grammar/vernacextend.cmo -COQPPCMO := grammar/coqpp_parse.cmo grammar/coqpp_lex.cmo +COQPPCMO := $(addsuffix .cmo, $(addprefix coqpp/, coqpp_parse coqpp_lex)) grammar/argextend.cmo : $(GRAMBASEDEPS) grammar/q_util.cmo : $(GRAMBASEDEPS) @@ -358,9 +358,9 @@ grammar/tacextend.cmo : $(GRAMBASEDEPS) grammar/argextend.cmo grammar/vernacextend.cmo : $(GRAMBASEDEPS) grammar/tacextend.cmo \ grammar/argextend.cmo -grammar/coqpp_parse.cmi: grammar/coqpp_ast.cmi -grammar/coqpp_parse.cmo: grammar/coqpp_ast.cmi grammar/coqpp_parse.cmi -grammar/coqpp_lex.cmo: grammar/coqpp_ast.cmi grammar/coqpp_parse.cmo +coqpp/coqpp_parse.cmi: coqpp/coqpp_ast.cmi +coqpp/coqpp_parse.cmo: coqpp/coqpp_ast.cmi coqpp/coqpp_parse.cmi +coqpp/coqpp_lex.cmo: coqpp/coqpp_ast.cmi coqpp/coqpp_parse.cmo ## Ocaml compiler with the right options and -I for grammar @@ -377,9 +377,9 @@ grammar/grammar.cma : $(GRAMCMO) $(SHOW)'OCAMLC -a $@' $(HIDE)$(GRAMC) $^ -linkall -a -o $@ -$(COQPP): $(COQPPCMO) grammar/coqpp_main.ml +$(COQPP): $(COQPPCMO) coqpp/coqpp_main.ml $(SHOW)'OCAMLC -a $@' - $(HIDE)$(GRAMC) $^ -linkall -o $@ + $(HIDE)$(GRAMC) -I coqpp $^ -linkall -o $@ ## Support of Camlp5 and Camlp5 diff --git a/Makefile.common b/Makefile.common index fdaa94212..727cb1e69 100644 --- a/Makefile.common +++ b/Makefile.common @@ -89,6 +89,7 @@ INSTALLSH:=./install.sh MKDIR:=install -d CORESRCDIRS:=\ + coqpp \ config clib lib kernel kernel/byterun library \ engine pretyping interp proofs parsing printing \ tactics vernac stm toplevel diff --git a/grammar/coqpp_ast.mli b/coqpp/coqpp_ast.mli index 39b4d2ab3..39b4d2ab3 100644 --- a/grammar/coqpp_ast.mli +++ b/coqpp/coqpp_ast.mli diff --git a/grammar/coqpp_lex.mll b/coqpp/coqpp_lex.mll index 6c6562c20..6c6562c20 100644 --- a/grammar/coqpp_lex.mll +++ b/coqpp/coqpp_lex.mll diff --git a/grammar/coqpp_main.ml b/coqpp/coqpp_main.ml index e76a1e9ed..e76a1e9ed 100644 --- a/grammar/coqpp_main.ml +++ b/coqpp/coqpp_main.ml diff --git a/grammar/coqpp_parse.mly b/coqpp/coqpp_parse.mly index baafd633c..baafd633c 100644 --- a/grammar/coqpp_parse.mly +++ b/coqpp/coqpp_parse.mly |