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

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

include ../Makefile.common