PACKAGE = tactics
REQUIRES = \
	pcre helm-cic_proof_checking \
	helm-cic_unification helm-mathql_interpreter helm-mathql_generator \
	mysql helm-metadata

INTERFACE_FILES = \
	proofEngineTypes.mli \
	proofEngineReduction.mli proofEngineHelpers.mli	\
	tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \
	primitiveTactics.mli hashtbl_equiv.mli metadataQuery.mli \
	variousTactics.mli autoTactic.mli \
	introductionTactics.mli	eliminationTactics.mli negationTactics.mli \
	equalityTactics.mli discriminationTactics.mli ring.mli fourier.mli \
	fourierR.mli history.mli statefulProofEngine.mli tactics.mli
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)

all:

tactics.mli: tactics.ml *Tactics.mli autoTactic.mli fourierR.mli ring.mli
	echo "(* GENERATED FILE, DO NOT EDIT *)" > $@
	$(OCAMLC) -i $< >> $@

include ../Makefile.common