]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_proof_checking/Makefile
fixed bug in fill_and_clean (now the helper universes_of_obj knows that
[helm.git] / helm / ocaml / cic_proof_checking / Makefile
1
2 PACKAGE = cic_proof_checking
3 REQUIRES = helm-cic helm-logger helm-getter helm-xml pxp
4 PREDICATES =
5
6 REDUCTION_IMPLEMENTATION = cicReductionMachine.ml
7
8 INTERFACE_FILES = \
9         cicLogger.mli \
10         cicEnvironment.mli \
11         cicPp.mli \
12         cicUnivUtils.mli \
13         cicSubstitution.mli \
14         cicMiniReduction.mli \
15         cicReductionNaif.mli \
16         cicReduction.mli \
17         cicTypeChecker.mli \
18         cicElim.mli
19 IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
20
21 # Metadata tools only need zeta-reduction
22 EXTRA_OBJECTS_TO_INSTALL = \
23             cicSubstitution.cmo cicSubstitution.cmx cicSubstitution.o \
24             cicMiniReduction.cmo cicMiniReduction.cmx cicMiniReduction.o
25 EXTRA_OBJECTS_TO_CLEAN =
26
27 include ../Makefile.common
28
29 cicReduction.ml: $(REDUCTION_IMPLEMENTATION)
30         if ! [ -f $@ ]; then \
31                 echo "Using $< for $@"; \
32                 ln -s $< $@;    \
33         else    \
34                 true;   \
35         fi
36