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

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

include ../Makefile.common