]> matita.cs.unibo.it Git - helm.git/blob - components/cic_proof_checking/Makefile
content2Procedural.ml: "Intros+LetTac" ok
[helm.git] / components / cic_proof_checking / Makefile
1
2 PACKAGE = cic_proof_checking
3 PREDICATES =
4
5 REDUCTION_IMPLEMENTATION = cicReductionMachine.ml
6
7 INTERFACE_FILES = \
8         cicLogger.mli \
9         cicEnvironment.mli \
10         cicPp.mli \
11         cicUnivUtils.mli \
12         cicSubstitution.mli \
13         cicMiniReduction.mli \
14         cicReduction.mli \
15         cicTypeChecker.mli \
16         freshNamesGenerator.mli \
17         $(NULL)
18 IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
19
20 # Metadata tools only need zeta-reduction
21 EXTRA_OBJECTS_TO_INSTALL = \
22             cicSubstitution.cmo cicSubstitution.cmx cicSubstitution.o \
23             cicMiniReduction.cmo cicMiniReduction.cmx cicMiniReduction.o
24 EXTRA_OBJECTS_TO_CLEAN =
25
26 include ../../Makefile.defs
27 include ../Makefile.common
28
29 cicReduction.cmo: OCAMLOPTIONS+=-rectypes
30 cicReduction.cmx: OCAMLOPTIONS+=-rectypes
31