aboutsummaryrefslogtreecommitdiff
path: root/Makefile.build
diff options
context:
space:
mode:
authorThéo Zimmermann2019-11-21 17:39:41 +0100
committerThéo Zimmermann2019-11-21 17:39:41 +0100
commita876df3f1e9a495ee04c78321adf83a31ede7f3c (patch)
treeda75e474f97b2434bc39fd877830b33c75982537 /Makefile.build
parentc0f34539209842735ccb93f3c069632b7eee4d6c (diff)
parentb4eca882b6692b6374dfff8517f9f5a5cc4970f5 (diff)
Merge PR #10614: Update the Gallina grammar in doc, "Terms" section
Ack-by: Zimmi48
Diffstat (limited to 'Makefile.build')
-rw-r--r--Makefile.build30
1 files changed, 0 insertions, 30 deletions
diff --git a/Makefile.build b/Makefile.build
index ff0e5dbaea..5b879220d0 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -363,36 +363,6 @@ $(COQPP): $(COQPPCMO) coqpp/coqpp_parser.mli coqpp/coqpp_parser.ml coqpp/coqpp_m
$(SHOW)'OCAMLC -a $@'
$(HIDE)$(OCAMLC) -I coqpp $^ -linkall -o $@
-DOC_GRAMCMO := $(addsuffix .cmo, $(addprefix coqpp/, coqpp_parse coqpp_lex))
-
-$(DOC_GRAM): $(DOC_GRAMCMO) coqpp/coqpp_parser.mli coqpp/coqpp_parser.ml doc/tools/docgram/doc_grammar.ml
- $(SHOW)'OCAMLC -a $@'
- $(HIDE)$(OCAMLC) -I coqpp $^ -package str -linkall -linkpkg -o $@
-
-DOC_MLGS := */*.mlg plugins/*/*.mlg
-DOC_EDIT_MLGS := doc/tools/docgram/*_mlg
-DOC_RSTS := doc/sphinx/*.rst doc/sphinx/*/*.rst
-
-doc/tools/docgram/fullGrammar: $(DOC_GRAM) $(DOC_MLGS)
- $(SHOW)'DOC_GRAM'
- $(HIDE)$(DOC_GRAM) -short -no-warn $(DOC_MLGS)
-
-#todo: add a dependency of sphinx on orderedGrammar and of *.rst on orderedGrammar when we're ready
-doc/tools/docgram/orderedGrammar: $(DOC_GRAM) $(DOC_EDIT_MLGS)
- $(SHOW)'DOC_GRAM_RSTS'
- $(HIDE)$(DOC_GRAM) $(DOC_MLGS) $(DOC_RSTS)
-
-.PHONY: doc_gram doc_gram_rsts doc_gram_verify
-
-doc_gram: doc/tools/docgram/fullGrammar
-
-doc_gram_verify: doc/tools/docgram/fullGrammar
- $(SHOW)'DOC_GRAM_VERIFY'
- $(HIDE)$(DOC_GRAM) -short -no-warn -verify $(DOC_MLGS) $(DOC_RSTS)
-
-#todo: add dependency on $(DOC_RSTS) very soon
-doc_gram_rsts: doc/tools/docgram/orderedGrammar
-
###########################################################################
# Specific rules for Uint63
###########################################################################