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

INTERFACE_FILES =	\
	proofEngineReduction.mli proofEngineHelpers.mli	\
	tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli	\
	primitiveTactics.mli variousTactics.mli introductionTactics.mli	\
	eliminationTactics.mli negationTactics.mli equalityTactics.mli	\
	discriminationTactics.mli ring.mli fourierR.mli tacticChaser.mli
IMPLEMENTATION_FILES =	\
	proofEngineTypes.ml proofEngineReduction.ml proofEngineHelpers.ml	\
	fourier.ml tacticals.ml reductionTactics.ml proofEngineStructuralRules.ml	\
	primitiveTactics.ml variousTactics.ml introductionTactics.ml	\
	eliminationTactics.ml negationTactics.ml equalityTactics.ml	\
	discriminationTactics.ml ring.ml fourierR.ml tacticChaser.ml


include ../Makefile.common