]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/tactics/Makefile
coercion application
[helm.git] / helm / ocaml / tactics / Makefile
1 PACKAGE = tactics
2 REQUIRES = \
3         pcre helm-cic_proof_checking \
4         helm-cic_unification helm-mathql_interpreter helm-mathql_generator \
5         mysql helm-metadata
6
7 INTERFACE_FILES = \
8         proofEngineTypes.mli \
9         proofEngineReduction.mli proofEngineHelpers.mli \
10         tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \
11         primitiveTactics.mli hashtbl_equiv.mli metadataQuery.mli \
12         variousTactics.mli autoTactic.mli \
13         introductionTactics.mli eliminationTactics.mli negationTactics.mli \
14         equalityTactics.mli discriminationTactics.mli ring.mli fourier.mli \
15         fourierR.mli history.mli statefulProofEngine.mli tactics.mli
16 IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
17
18 all:
19
20 tactics.mli: tactics.ml *Tactics.mli autoTactic.mli fourierR.mli ring.mli
21         echo "(* GENERATED FILE, DO NOT EDIT *)" > $@
22         $(OCAMLC) -i $< >> $@
23
24 include ../Makefile.common
25