X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FMakefile;h=b576f830b5f94909acd7e9f893b8eeff74a2d1fd;hb=9655a931c73be820d876da7b23fe54b55fd60c14;hp=cdb16efe466ab2eca4a476efc82e92b959a1439f;hpb=06b128f1107fd579a696b83b2f8255f83ab29a92;p=helm.git diff --git a/components/tactics/Makefile b/components/tactics/Makefile index cdb16efe4..b576f830b 100644 --- a/components/tactics/Makefile +++ b/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,11 +18,11 @@ INTERFACE_FILES = \ paramodulation/indexing.mli \ paramodulation/saturation.mli \ variousTactics.mli \ + compose.mli \ introductionTactics.mli eliminationTactics.mli negationTactics.mli \ equalityTactics.mli \ auto.mli \ - autoTactic.mli \ - discriminationTactics.mli \ + discriminationTactics.mli substTactic.mli \ inversion.mli inversion_principle.mli ring.mli setoids.mli \ fourier.mli fourierR.mli fwdSimplTactic.mli history.mli \ statefulProofEngine.mli tactics.mli declarative.mli @@ -57,3 +58,5 @@ include ../Makefile.common OCAMLOPTIONS+= -I paramodulation OCAMLDEPOPTIONS+= -I paramodulation +#PREPROCOPTIONS:= +#OCAML_PROF=p -p a