]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/tactics/Makefile
Added new module DiscriminationTactics
[helm.git] / helm / ocaml / tactics / Makefile
1 PACKAGE = tactics
2 REQUIRES = helm-cic_textual_parser helm-cic_proof_checking helm-cic_unification
3
4 INTERFACE_FILES =       \
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      \
10         fourierR.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        \
17         fourierR.ml
18
19
20 include ../Makefile.common
21