2 REQUIRES = helm-cic_textual_parser helm-cic_proof_checking helm-cic_unification
5 proofEngineReduction.mli proofEngineHelpers.mli \
6 tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \
7 primitiveTactics.mli variousTactics.mli introductionTactics.mli \
8 eliminationTactics.mli negationTactics.mli equalityTactics.mli \
9 discriminationTactics.mli ring.mli \
11 IMPLEMENTATION_FILES = \
12 proofEngineTypes.ml proofEngineReduction.ml proofEngineHelpers.ml \
13 fourier.ml tacticals.ml reductionTactics.ml proofEngineStructuralRules.ml \
14 primitiveTactics.ml variousTactics.ml introductionTactics.ml \
15 eliminationTactics.ml negationTactics.ml equalityTactics.ml \
16 discriminationTactics.ml ring.ml \
20 include ../Makefile.common