5 proofEngineHelpers.mli proofEngineReduction.mli \
7 tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \
8 primitiveTactics.mli hashtbl_equiv.mli metadataQuery.mli \
9 paramodulation/utils.mli \
10 paramodulation/equality.mli\
11 paramodulation/inference.mli\
12 paramodulation/equality_indexing.mli\
13 paramodulation/indexing.mli \
14 paramodulation/saturation.mli \
15 variousTactics.mli autoTactic.mli \
16 introductionTactics.mli eliminationTactics.mli negationTactics.mli \
17 equalityTactics.mli discriminationTactics.mli inversion.mli \
18 inversion_principle.mli ring.mli \
19 fourier.mli fourierR.mli fwdSimplTactic.mli history.mli \
20 statefulProofEngine.mli tactics.mli
22 IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
27 # we omit dependencies since it is a pain when distributing
28 tactics_mli_deps=tactics.ml *Tactics.mli *Tactic.mli fourierR.mli ring.mli paramodulation/indexing.mli
30 $(H)echo " OCAMLC -i $$(tactics_mli_deps) > $@"
31 $(H)echo "(* GENERATED FILE, DO NOT EDIT. STAMP:`date` *)" > $@
32 $(H)$(OCAMLC) -I paramodulation -i $(tactics_mli_deps) >> $@
34 STATS_EXCLUDE = tactics.mli
36 include ../../Makefile.defs
37 include ../Makefile.common
39 OCAMLOPTIONS+= -I paramodulation
40 OCAMLDEPOPTIONS+= -I paramodulation