- tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \
- primitiveTactics.mli variousTactics.mli introductionTactics.mli \
- eliminationTactics.mli negationTactics.mli equalityTactics.mli \
- discriminationTactics.mli ring.mli fourierR.mli tacticChaser.mli
-IMPLEMENTATION_FILES = \
- proofEngineTypes.ml proofEngineReduction.ml proofEngineHelpers.ml \
- fourier.ml tacticals.ml reductionTactics.ml proofEngineStructuralRules.ml \
- primitiveTactics.ml variousTactics.ml introductionTactics.ml \
- eliminationTactics.ml negationTactics.ml equalityTactics.ml \
- discriminationTactics.ml ring.ml fourierR.ml tacticChaser.ml
-
+ tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \
+ primitiveTactics.mli tacticChaser.mli variousTactics.mli \
+ introductionTactics.mli eliminationTactics.mli negationTactics.mli \
+ equalityTactics.mli discriminationTactics.mli ring.mli fourier.mli \
+ fourierR.mli statefulProofEngine.mli
+IMPLEMENTATION_FILES = proofEngineTypes.ml $(INTERFACE_FILES:%.mli=%.ml)