aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/CoqMakefile.in
diff options
context:
space:
mode:
Diffstat (limited to 'tools/CoqMakefile.in')
-rw-r--r--tools/CoqMakefile.in9
1 files changed, 0 insertions, 9 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 2ebe4aba7..872a73282 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -86,7 +86,6 @@ COQC ?= "$(COQBIN)coqc"
COQTOP ?= "$(COQBIN)coqtop"
COQCHK ?= "$(COQBIN)coqchk"
COQDEP ?= "$(COQBIN)coqdep"
-GALLINA ?= "$(COQBIN)gallina"
COQDOC ?= "$(COQBIN)coqdoc"
COQMKFILE ?= "$(COQBIN)coq_makefile"
@@ -256,7 +255,6 @@ VO = vo
VOFILES = $(VFILES:.v=.$(VO))
GLOBFILES = $(VFILES:.v=.glob)
-GFILES = $(VFILES:.v=.g)
HTMLFILES = $(VFILES:.v=.html)
GHTMLFILES = $(VFILES:.v=.g.html)
BEAUTYFILES = $(addsuffix .beautified,$(VFILES))
@@ -442,8 +440,6 @@ all-mli.tex: $(MLIFILES:.mli=.cmi)
$(HIDE)$(CAMLDOC) -latex \
-o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES)
-gallina: $(GFILES)
-
all.ps: $(VFILES)
$(SHOW)'COQDOC -ps $(GAL)'
$(HIDE)$(COQDOC) \
@@ -564,7 +560,6 @@ clean::
$(HIDE)find . -name .coq-native -type d -empty -delete
$(HIDE)rm -f $(VOFILES)
$(HIDE)rm -f $(VOFILES:.vo=.vio)
- $(HIDE)rm -f $(GFILES)
$(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old)
$(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex
$(HIDE)rm -f $(VFILES:.v=.glob)
@@ -683,10 +678,6 @@ $(BEAUTYFILES): %.v.beautified: %.v
$(SHOW)'BEAUTIFY $<'
$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -beautify $<
-$(GFILES): %.g: %.v
- $(SHOW)'GALLINA $<'
- $(HIDE)$(GALLINA) $<
-
$(TEXFILES): %.tex: %.v
$(SHOW)'COQDOC -latex $<'
$(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@