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/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 ring.mli \ fourier.mli fourierR.mli fwdSimplTactic.mli history.mli \ statefulProofEngine.mli tactics.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) all: tactics.mli: tactics.ml *Tactics.mli *Tactic.mli fourierR.mli ring.mli paramodulation/indexing.mli @echo " OCAMLC -i $< > $@" $(H)echo "(* GENERATED FILE, DO NOT EDIT *)" > $@ $(H)$(OCAMLC) -I paramodulation -i $< >> $@ STATS_EXCLUDE = tactics.mli include ../../Makefile.defs include ../Makefile.common OCAMLOPTIONS+= -I paramodulation OCAMLDEPOPTIONS+= -I paramodulation