]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_proof_checking/Makefile
0259effd12d2a9239c6d3d69fe1657902c5bb863
[helm.git] / helm / ocaml / cic_proof_checking / Makefile
1 PACKAGE = cic_proof_checking
2 REQUIRES = helm-cic
3 PREDICATES =
4
5 REDUCTION_IMPLEMENTATION = cicReductionMachine.ml
6
7 INTERFACE_FILES = logger.mli cicEnvironment.mli cicPp.mli cicSubstitution.mli \
8                   cicMiniReduction.mli cicReductionNaif.mli cicReduction.mli \
9                   cicTypeChecker.mli
10 IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
11
12 # Metadata tools only need zeta-reduction
13 EXTRA_OBJECTS_TO_INSTALL = \
14             cicSubstitution.cmo cicSubstitution.cmx cicSubstitution.o \
15             cicMiniReduction.cmo cicMiniReduction.cmx cicMiniReduction.o
16 EXTRA_OBJECTS_TO_CLEAN =
17
18 include ../Makefile.common
19
20 cicReduction.ml: $(REDUCTION_IMPLEMENTATION)
21         if ! [ -f $@ ]; then \
22                 echo "Using $< for $@"; \
23                 ln -s $< $@;    \
24         else    \
25                 true;   \
26         fi
27