diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-07-11 14:35:16 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-07-11 14:35:16 +0200 |
| commit | bd0a681350b1bc8947d6d7603dc6a9759f0c7897 (patch) | |
| tree | b7381958c8442a17a6e403251608e4d5f80d520d | |
| parent | b646ab446866160b3c657f0134e93fdf002cbc7f (diff) | |
| parent | dd25b08c3608b55dd9edb24304168efb56bc64c8 (diff) | |
Merge PR #7998: [coqpp] Move to its own directory.
| -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 |