PACKAGE = tactics

INTERFACE_FILES = \
	proofEngineTypes.mli \
	proofEngineHelpers.mli proofEngineReduction.mli \
	continuationals.mli \
	tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \
	primitiveTactics.mli hashtbl_equiv.mli metadataQuery.mli \
  paramodulation/utils.mli \
  paramodulation/equality.mli\
  paramodulation/inference.mli\
  paramodulation/equality_indexing.mli\
  paramodulation/indexing.mli \
  paramodulation/saturation.mli \
	variousTactics.mli autoTactic.mli \
	introductionTactics.mli	eliminationTactics.mli negationTactics.mli \
	equalityTactics.mli discriminationTactics.mli inversion.mli \
	inversion_principle.mli ring.mli \
	fourier.mli fourierR.mli fwdSimplTactic.mli history.mli \
	statefulProofEngine.mli tactics.mli

IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)


all:

# we omit dependencies since it is a pain when distributing
tactics_mli_deps=tactics.ml *Tactics.mli *Tactic.mli fourierR.mli ring.mli paramodulation/indexing.mli
tactics.mli: 
	$(H)echo "  OCAMLC -i $$(tactics_mli_deps) > $@"
	$(H)echo "(* GENERATED FILE, DO NOT EDIT. STAMP:`date` *)" > $@
	$(H)$(OCAMLC) -I paramodulation -i $(tactics_mli_deps) >> $@

STATS_EXCLUDE = tactics.mli

include ../../Makefile.defs
include ../Makefile.common

OCAMLOPTIONS+= -I paramodulation
OCAMLDEPOPTIONS+= -I paramodulation