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