]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/tactics/Makefile
- the mathql interpreter is not helm-dependent any more
[helm.git] / helm / ocaml / tactics / Makefile
1 PACKAGE = tactics
2 REQUIRES = \
3         helm-cic_textual_parser helm-cic_proof_checking helm-cic_unification \
4         helm-mathql_interpreter helm-mathql_generator
5
6 INTERFACE_FILES =       \
7         proofEngineReduction.mli proofEngineHelpers.mli \
8         tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli       \
9         primitiveTactics.mli variousTactics.mli introductionTactics.mli \
10         eliminationTactics.mli negationTactics.mli equalityTactics.mli  \
11         discriminationTactics.mli ring.mli fourierR.mli tacticChaser.mli
12 IMPLEMENTATION_FILES =  \
13         proofEngineTypes.ml proofEngineReduction.ml proofEngineHelpers.ml       \
14         fourier.ml tacticals.ml reductionTactics.ml proofEngineStructuralRules.ml       \
15         primitiveTactics.ml variousTactics.ml introductionTactics.ml    \
16         eliminationTactics.ml negationTactics.ml equalityTactics.ml     \
17         discriminationTactics.ml ring.ml fourierR.ml tacticChaser.ml
18
19
20 include ../Makefile.common
21