paramodulation/saturation.mli \
variousTactics.mli autoTactic.mli \
introductionTactics.mli eliminationTactics.mli negationTactics.mli \
- equalityTactics.mli discriminationTactics.mli inversion.mli ring.mli \
+ equalityTactics.mli discriminationTactics.mli inversion.mli \
+ inversion_principle.mli ring.mli \
fourier.mli fourierR.mli fwdSimplTactic.mli history.mli \
statefulProofEngine.mli tactics.mli
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 $< >> $@
+# 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