X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FMakefile;h=c4e020005e0a8ea4462aa678a88e08aa57062bab;hb=683978a2627cf1ce15673360f26806593d22f7b5;hp=8990812993d9e897b9a88761ea8e286e69fec930;hpb=cf4088e2cabcbce9b112f1e1fd5cfd38fe16d427;p=helm.git diff --git a/helm/software/components/tactics/Makefile b/helm/software/components/tactics/Makefile index 899081299..c4e020005 100644 --- a/helm/software/components/tactics/Makefile +++ b/helm/software/components/tactics/Makefile @@ -10,6 +10,7 @@ INTERFACE_FILES = \ autoTypes.mli \ autoCache.mli \ paramodulation/utils.mli \ + closeCoercionGraph.mli \ paramodulation/subst.mli \ paramodulation/equality.mli\ paramodulation/founif.mli\ @@ -17,6 +18,7 @@ INTERFACE_FILES = \ paramodulation/indexing.mli \ paramodulation/saturation.mli \ variousTactics.mli \ + compose.mli \ introductionTactics.mli eliminationTactics.mli negationTactics.mli \ equalityTactics.mli \ auto.mli \ @@ -40,7 +42,7 @@ tactics.mli: tactics.ml UTF8DIR = $(shell $(OCAMLFIND) query helm-syntax_extensions) STR=$(shell $(OCAMLFIND) query str) -MY_SYNTAXOPTIONS = -pp "camlp4o -I $(UTF8DIR) -I $(STR) str.cma pa_extend.cmo profiling_macros.cma -loc loc" +MY_SYNTAXOPTIONS = -pp "camlp5o -I $(UTF8DIR) -I $(STR) str.cma pa_extend.cmo profiling_macros.cma -loc loc" paramodulation/%.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) paramodulation/%.cmo: OCAMLC = $(OCAMLC_P4) paramodulation/%.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) @@ -56,3 +58,5 @@ include ../Makefile.common OCAMLOPTIONS+= -I paramodulation OCAMLDEPOPTIONS+= -I paramodulation +#PREPROCOPTIONS:= +#OCAML_PROF=p -p a