X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FMakefile;h=c4e020005e0a8ea4462aa678a88e08aa57062bab;hb=683978a2627cf1ce15673360f26806593d22f7b5;hp=e6f63eac0a5ee0e9e28018d161f1a1b5efc84c38;hpb=f438e9b0c8e43a66c56b17adeb8793042d0aade1;p=helm.git diff --git a/helm/software/components/tactics/Makefile b/helm/software/components/tactics/Makefile index e6f63eac0..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)