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 = $(INTERFACE_FILES:%.mli=%.ml) include ../Makefile.common