aboutsummaryrefslogtreecommitdiffstats
path: root/src/versions/native/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'src/versions/native/Makefile')
-rw-r--r--src/versions/native/Makefile505
1 files changed, 0 insertions, 505 deletions
diff --git a/src/versions/native/Makefile b/src/versions/native/Makefile
deleted file mode 100644
index aaaab9e..0000000
--- a/src/versions/native/Makefile
+++ /dev/null
@@ -1,505 +0,0 @@
-#############################################################################
-## v # The Coq Proof Assistant ##
-## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
-## \VV/ # ##
-## // # Makefile automagically generated by coq_makefile Vtrunk ##
-#############################################################################
-
-# WARNING
-#
-# This Makefile has been automagically generated
-# Edit at your own risks !
-#
-# END OF WARNING
-
-#
-# This Makefile was generated by the command line :
-# coq_makefile -f Make -o Makefile
-#
-
-.DEFAULT_GOAL := all
-
-#
-# This Makefile may take arguments passed as environment variables:
-# COQBIN to specify the directory where Coq binaries resides;
-# ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc;
-# DSTROOT to specify a prefix to install path.
-
-# Here is a hack to make $(eval $(shell works:
-define donewline
-
-
-endef
-includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr '\n' '@'; })))
-$(call includecmdwithout@,$(COQBIN)coqtop -config)
-
-##########################
-# #
-# Libraries definitions. #
-# #
-##########################
-
-OCAMLLIBS?=-I ../3rdparty/alt-ergo\
- -I versions/native\
- -I zchaff\
- -I verit\
- -I trace\
- -I smtlib2\
- -I lia\
- -I lfsc\
- -I euf\
- -I cnf\
- -I array\
- -I classes\
- -I bva
-COQLIBS?=-I ../3rdparty/alt-ergo\
- -I versions/native\
- -I zchaff\
- -I verit\
- -I trace\
- -I smtlib2\
- -I lia\
- -I lfsc\
- -I euf\
- -I cnf\
- -I array\
- -I classes\
- -I bva -R . SMTCoq
-COQDOCLIBS?=-R . SMTCoq
-
-##########################
-# #
-# Variables definitions. #
-# #
-##########################
-
-CAMLYACC=$(CAMLBIN)ocamlyacc
-CAMLLEX=$(CAMLBIN)ocamllex
-VCMXS=versions/native/NSMTCoq_versions_native_Structures.cmxs NSMTCoq_State.cmxs NSMTCoq_Misc.cmxs classes/NSMTCoq_SMT_classes.cmxs classes/NSMTCoq_SMT_classes_instances.cmxs NSMTCoq_SMT_terms.cmxs cnf/NSMTCoq_cnf_Cnf.cmxs euf/NSMTCoq_euf_Euf.cmxs lia/NSMTCoq_lia_Lia.cmxs spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Assumptions.cmxs spl/NSMTCoq_spl_Arithmetic.cmxs spl/NSMTCoq_spl_Operators.cmxs NSMTCoq_Trace.cmxs NSMTCoq_Tactics.cmxs NSMTCoq_Conversion_tactics.cmxs NSMTCoq_PropToBool.cmxs NSMTCoq_BoolToProp.cmxs NSMTCoq_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.cmi classes/NSMTCoq_SMT_classes.cmi classes/NSMTCoq_SMT_classes_instances.cmi NSMTCoq_SMT_terms.cmi cnf/NSMTCoq_cnf_Cnf.cmi euf/NSMTCoq_euf_Euf.cmi lia/NSMTCoq_lia_Lia.cmi spl/NSMTCoq_spl_Syntactic.cmi spl/NSMTCoq_spl_Assumptions.cmi spl/NSMTCoq_spl_Arithmetic.cmi spl/NSMTCoq_spl_Operators.cmi NSMTCoq_Trace.cmi NSMTCoq_Trace.cmi NSMTCoq_Tactics.cmi NSMTCoq_Conversion_tactics.cmi NSMTCoq_PropToBool.cmi NSMTCoq_BoolToProp.cmi NSMTCoq_SMTCoq.cmi
-CMXS=smtcoq_plugin.cmxs
-CMXA=smtcoq.cmxa
-
-OPT?=
-COQDEP?=$(COQBIN)coqdep -c
-COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
-COQCHKFLAGS?=-silent -o
-COQDOCFLAGS?=-interpolate -utf8
-COQC?=$(COQBIN)coqc
-GALLINA?=$(COQBIN)gallina
-COQDOC?=$(COQBIN)coqdoc
-COQCHK?=$(COQBIN)coqchk
-
-COQSRCLIBS?=-I $(COQLIB)kernel -I $(COQLIB)lib \
- -I $(COQLIB)library -I $(COQLIB)parsing \
- -I $(COQLIB)pretyping -I $(COQLIB)interp \
- -I $(COQLIB)proofs -I $(COQLIB)tactics \
- -I $(COQLIB)toplevel \
- -I $(COQLIB)plugins/btauto \
- -I $(COQLIB)plugins/cc \
- -I $(COQLIB)plugins/decl_mode \
- -I $(COQLIB)plugins/extraction \
- -I $(COQLIB)plugins/field \
- -I $(COQLIB)plugins/firstorder \
- -I $(COQLIB)plugins/fourier \
- -I $(COQLIB)plugins/funind \
- -I $(COQLIB)plugins/micromega \
- -I $(COQLIB)plugins/nsatz \
- -I $(COQLIB)plugins/omega \
- -I $(COQLIB)plugins/quote \
- -I $(COQLIB)plugins/ring \
- -I $(COQLIB)plugins/romega \
- -I $(COQLIB)plugins/rtauto \
- -I $(COQLIB)plugins/setoid_ring \
- -I $(COQLIB)plugins/syntax \
- -I $(COQLIB)plugins/xml
-ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)
-
-CAMLC?=$(OCAMLC) -c -rectypes
-CAMLOPTC?=$(OCAMLOPT) -c -rectypes
-CAMLLINK?=$(OCAMLC) -rectypes
-CAMLOPTLINK?=$(OCAMLOPT) -rectypes
-GRAMMARS?=grammar.cma
-CAMLP4EXTEND?=pa_extend.cmo pa_macro.cmo q_MLast.cmo
-CAMLP4OPTIONS?=-loc loc
-PP?=-pp "$(CAMLP4BIN)$(CAMLP4)o -I $(CAMLLIB) -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl"
-
-##################
-# #
-# Install Paths. #
-# #
-##################
-
-ifdef USERINSTALL
-XDG_DATA_HOME?=$(HOME)/.local/share
-COQLIBINSTALL=$(XDG_DATA_HOME)/coq
-COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq
-else
-COQLIBINSTALL=${COQLIB}user-contrib
-COQDOCINSTALL=${DOCDIR}user-contrib
-endif
-
-######################
-# #
-# Files dispatching. #
-# #
-######################
-
-VFILES:=Trace.v\
- State.v\
- SMT_terms.v\
- Tactics.v\
- BoolToProp.v\
- PropToBool.v\
- ReflectFacts.v\
- SMTCoq.v\
- Misc.v\
- Conversion_tactics.v\
- spl/Operators.v\
- spl/Arithmetic.v\
- spl/Syntactic.v\
- spl/Assumptions.v\
- lia/Lia.v\
- euf/Euf.v\
- cnf/Cnf.v\
- versions/native/Structures.v\
- array/Array_checker.v\
- array/FArray.v\
- classes/SMT_classes_instances.v\
- classes/SMT_classes.v\
- bva/Bva_checker.v\
- bva/BVList.v
-
--include $(addsuffix .d,$(VFILES))
-.SECONDARY: $(addsuffix .d,$(VFILES))
-
-vo_to_obj = $(addsuffix .o,$(foreach vo,$(1),$(addprefix $(dir $(vo)),$(filter-out Warning: Error:,$(firstword $(shell $(COQBIN)coqtop -batch -quiet -print-mod-uid $(vo:.vo=)))))))
-VOFILES:=$(foreach vo,$(VFILES:.v=.vo),$(dir $(vo))$(notdir $(vo)))
-GLOBFILES:=$(VFILES:.v=.glob)
-VIFILES:=$(VFILES:.v=.vi)
-GFILES:=$(VFILES:.v=.g)
-HTMLFILES:=$(VFILES:.v=.html)
-GHTMLFILES:=$(VFILES:.v=.g.html)
-OBJFILES:=$(call vo_to_obj,$(VOFILES))
-ML4FILES:=smtcoq_plugin.ml4
-
--include $(addsuffix .d,$(ML4FILES))
-.SECONDARY: $(addsuffix .d,$(ML4FILES))
-
-MLFILES:=lia/lia.ml\
- zchaff/zchaffParser.ml\
- zchaff/zchaff.ml\
- zchaff/satParser.ml\
- zchaff/cnfParser.ml\
- lfsc/lfsc.ml\
- lfsc/converter.ml\
- lfsc/tosmtcoq.ml\
- lfsc/builtin.ml\
- lfsc/ast.ml\
- lfsc/type.ml\
- lfsc/lfscLexer.ml\
- lfsc/lfscParser.ml\
- lfsc/hstring.ml\
- lfsc/shashcons.ml\
- verit/veritSyntax.ml\
- verit/verit.ml\
- verit/veritLexer.ml\
- verit/veritParser.ml\
- smtlib2/smtlib2_solver.ml\
- smtlib2/sExpr.ml\
- smtlib2/sExprLexer.ml\
- smtlib2/sExprParser.ml\
- smtlib2/smtlib2_genConstr.ml\
- ../3rdparty/alt-ergo/smtlib2_util.ml\
- ../3rdparty/alt-ergo/smtlib2_ast.ml\
- ../3rdparty/alt-ergo/smtlib2_lex.ml\
- ../3rdparty/alt-ergo/smtlib2_parse.ml\
- trace/smtTrace.ml\
- trace/smtMisc.ml\
- trace/smtMaps.ml\
- trace/smtForm.ml\
- trace/smtCommands.ml\
- trace/smtCnf.ml\
- trace/smtCertif.ml\
- trace/smtBtype.ml\
- trace/smtAtom.ml\
- trace/satAtom.ml\
- trace/coqTerms.ml\
- versions/native/structures.ml
-
--include $(addsuffix .d,$(MLFILES))
-.SECONDARY: $(addsuffix .d,$(MLFILES))
-
-MLIFILES:=lia/lia.mli\
- zchaff/zchaffParser.mli\
- zchaff/zchaff.mli\
- zchaff/satParser.mli\
- zchaff/cnfParser.mli\
- lfsc/tosmtcoq.mli\
- lfsc/translator_sig.mli\
- lfsc/ast.mli\
- lfsc/hstring.mli\
- lfsc/shashcons.mli\
- verit/veritSyntax.mli\
- verit/verit.mli\
- verit/veritLexer.mli\
- verit/veritParser.mli\
- smtlib2/smtlib2_solver.mli\
- smtlib2/sExpr.mli\
- smtlib2/sExprParser.mli\
- smtlib2/smtlib2_genConstr.mli\
- ../3rdparty/alt-ergo/smtlib2_util.mli\
- ../3rdparty/alt-ergo/smtlib2_ast.mli\
- ../3rdparty/alt-ergo/smtlib2_lex.mli\
- ../3rdparty/alt-ergo/smtlib2_parse.mli\
- trace/smtTrace.mli\
- trace/smtMisc.mli\
- trace/smtMaps.mli\
- trace/smtForm.mli\
- trace/smtCommands.mli\
- trace/smtCnf.mli\
- trace/smtCertif.mli\
- trace/smtBtype.mli\
- trace/smtAtom.mli\
- trace/satAtom.mli\
- trace/coqTerms.mli\
- versions/native/structures.mli
-
--include $(addsuffix .d,$(MLIFILES))
-.SECONDARY: $(addsuffix .d,$(MLIFILES))
-
-ALLCMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLFILES:.ml=.cmo)
-CMOFILES=$(filter-out $(addsuffix .cmo,$(foreach lib,$(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES) $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ALLCMOFILES))
-CMXFILES=$(CMOFILES:.cmo=.cmx)
-CMIFILES=$(sort $(ALLCMOFILES:.cmo=.cmi) $(MLIFILES:.mli=.cmi))
-CMXSFILES=$(CMXFILES:.cmx=.cmxs)
-
-#######################################
-# #
-# Definition of the toplevel targets. #
-# #
-#######################################
-
-all: ml $(CMXFILES) $(CMXA) $(CMXS) $(VOFILES)
-
-mlihtml: $(MLIFILES:.mli=.cmi)
- mkdir $@ || rm -rf $@/*
- $(OCAMLDOC) -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)
-
-all-mli.tex: $(MLIFILES:.mli=.cmi)
- $(OCAMLDOC) -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)
-
-spec: $(VIFILES)
-
-gallina: $(GFILES)
-
-html: $(GLOBFILES) $(VFILES)
- - mkdir -p html
- $(COQDOC) -toc $(COQDOCFLAGS) -html $(COQDOCLIBS) -d html $(VFILES)
-
-gallinahtml: $(GLOBFILES) $(VFILES)
- - mkdir -p html
- $(COQDOC) -toc $(COQDOCFLAGS) -html -g $(COQDOCLIBS) -d html $(VFILES)
-
-all.ps: $(VFILES)
- $(COQDOC) -toc $(COQDOCFLAGS) -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
-
-all-gal.ps: $(VFILES)
- $(COQDOC) -toc $(COQDOCFLAGS) -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
-
-all.pdf: $(VFILES)
- $(COQDOC) -toc $(COQDOCFLAGS) -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
-
-all-gal.pdf: $(VFILES)
- $(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
-
-validate: $(VOFILES)
- $(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $(notdir $(^:.vo=))
-
-beautify: $(VFILES:=.beautified)
- for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done
- @echo 'Do not do "make clean" until you are sure that everything went well!'
- @echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/'
-
-.PHONY: all opt byte archclean clean install userinstall depend html validate
-
-###################
-# #
-# Custom targets. #
-# #
-###################
-
-$(CMXS): $(CMXA)
- $(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^
-
-$(CMXA): versions/native/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtBtype.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx trace/smtMaps.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx ../3rdparty/alt-ergo/smtlib2_util.cmx ../3rdparty/alt-ergo/smtlib2_ast.cmx ../3rdparty/alt-ergo/smtlib2_parse.cmx ../3rdparty/alt-ergo/smtlib2_lex.cmx smtlib2/sExpr.cmx smtlib2/sExprParser.cmx smtlib2/sExprLexer.cmx smtlib2/smtlib2_solver.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx lfsc/shashcons.cmx lfsc/hstring.cmx lfsc/type.cmx lfsc/ast.cmx lfsc/builtin.cmx lfsc/tosmtcoq.cmx lfsc/converter.cmx lfsc/lfscParser.cmx lfsc/lfscLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx lfsc/lfsc.cmx smtcoq_plugin.cmx
- $(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^
-
-ml: verit/veritParser.ml verit/veritLexer.ml ../3rdparty/alt-ergo/smtlib2_parse.ml ../3rdparty/alt-ergo/smtlib2_lex.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml
-
-
-%.ml %.mli: %.mly
- $(CAMLYACC) $<
-
-%.ml: %.mll
- $(CAMLLEX) $<
-
-vtest:
- cd ../unit-tests; make veritv
-
-ztest:
- cd ../unit-tests; make zchaffv
-
-test:
- cd ../unit-tests; make vernac
-
-####################
-# #
-# Special targets. #
-# #
-####################
-
-byte:
- $(MAKE) all "OPT:=-byte"
-
-opt:
- $(MAKE) all "OPT:=-opt"
-
-userinstall:
- +$(MAKE) USERINSTALL=true install
-
-install-natdynlink:
- for i in $(CMXS); do \
- install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
- install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
- done
- for i in $(CMXA); do \
- install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
- install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
- done
- for i in $(VCMXS); do \
- install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
- install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
- done
-
-install:$(if ifeq '$(HASNATDYNLINK)' 'true',install-natdynlink)
- for i in $(VOFILES) $(OBJFILES) $(OBJFILES:.o=.cm*); do \
- install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
- install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
- done
- for i in $(CMXFILES); do \
- install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
- install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
- done
- for i in $(CMIFILES); do \
- install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
- install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
- done
-
-install-doc:
- install -d $(DSTROOT)$(COQDOCINSTALL)/SMTCoq/html
- for i in html/*; do \
- install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/SMTCoq/$$i;\
- done
- install -d $(DSTROOT)$(COQDOCINSTALL)/SMTCoq/mlihtml
- for i in mlihtml/*; do \
- install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/SMTCoq/$$i;\
- done
-
-clean:
- rm -f $(ALLCMOFILES) $(CMIFILES) $(CMAFILES)
- rm -f $(ALLCMOFILES:.cmo=.cmx) $(CMXAFILES) $(CMXSFILES) $(ALLCMOFILES:.cmo=.o) $(CMXAFILES:.cmxa=.a)
- rm -f $(addsuffix .d,$(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(MLPACKFILES))
- rm -f $(OBJFILES) $(OBJFILES:.o=.native)
- rm -f $(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo)
- rm -f $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)
- rm -f $(VOFILES) $(VIFILES) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)
- rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex
- - rm -rf html mlihtml
- - rm -rf $(CMXS)
- - rm -rf $(CMXA)
- - rm -rf ml
- - rm -rf vtest
- - rm -rf ztest
- - rm -rf test
- - rm -f NSMTCoq* cnf/NSMTCoq* euf/NSMTCoq* lia/NSMTCoq* spl/NSMTCoq* ../unit-tests/NSMTCoq* ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml ../3rdparty/alt-ergo/smtlib2_parse.mli ../3rdparty/alt-ergo/smtlib2_parse.ml ../3rdparty/alt-ergo/smtlib2_lex.ml smtlib2/sExprParser.mli smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscLexer.ml lfsc/lfscParser.ml lfsc/lfscParser.mli trace/smtcoq.a
-
-archclean:
- rm -f *.cmx *.o
-
-printenv:
- @$(COQBIN)coqtop -config
- @echo CAMLC = $(CAMLC)
- @echo CAMLOPTC = $(CAMLOPTC)
- @echo PP = $(PP)
- @echo COQFLAGS = $(COQFLAGS)
- @echo COQLIBINSTALL = $(COQLIBINSTALL)
- @echo COQDOCINSTALL = $(COQDOCINSTALL)
-
-
-###################
-# #
-# Implicit rules. #
-# #
-###################
-
-%.cmi: %.mli
- $(CAMLC) $(ZDEBUG) $(ZFLAGS) $<
-
-%.mli.d: %.mli
- $(OCAMLDEP) -slash $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
-
-%.cmo: %.ml4
- $(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<
-
-%.cmx: %.ml4
- $(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<
-
-%.ml4.d: %.ml4
- $(OCAMLDEP) -slash $(OCAMLLIBS) $(PP) -impl "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
-
-%.cmo: %.ml
- $(CAMLC) $(ZDEBUG) $(ZFLAGS) $<
-
-%.cmx: %.ml
- $(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<
-
-%.ml.d: %.ml
- $(OCAMLDEP) -slash $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
-
-%.cmxs: %.cmx
- $(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<
-
-%.vo %.glob: %.v
- $(COQC) $(COQDEBUG) $(COQFLAGS) $*
-
-%.vi: %.v
- $(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
-
-%.g: %.v
- $(GALLINA) $<
-
-%.tex: %.v
- $(COQDOC) $(COQDOCFLAGS) -latex $< -o $@
-
-%.html: %.v %.glob
- $(COQDOC) $(COQDOCFLAGS) -html $< -o $@
-
-%.g.tex: %.v
- $(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
-
-%.g.html: %.v %.glob
- $(COQDOC)$(COQDOCFLAGS) -html -g $< -o $@
-
-%.v.d: %.v
- $(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
-
-%.v.beautified:
- $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*
-
-# WARNING
-#
-# This Makefile has been automagically generated
-# Edit at your own risks !
-#
-# END OF WARNING
-