X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FMakefile;h=aa16069976a5c9461407fc0007382b08c21a1dd5;hb=acfce0988db6cce820044b174f4f485dc0a0c6ec;hp=f3e3a37a06c09e951ded3cb72ed8d77015ea591a;hpb=cc3ab906b631ef0edb4402cb622fc3fa96682717;p=helm.git diff --git a/helm/software/components/tactics/Makefile b/helm/software/components/tactics/Makefile index f3e3a37a0..aa1606997 100644 --- a/helm/software/components/tactics/Makefile +++ b/helm/software/components/tactics/Makefile @@ -6,19 +6,19 @@ INTERFACE_FILES = \ continuationals.mli \ tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \ primitiveTactics.mli hashtbl_equiv.mli metadataQuery.mli \ - paramodulation/utils.mli \ - paramodulation/subst.mli\ - paramodulation/equality.mli\ - paramodulation/inference.mli\ - paramodulation/equality_indexing.mli\ - paramodulation/indexing.mli \ - paramodulation/saturation.mli \ + paramodulation/utils.mli \ + paramodulation/subst.mli\ + paramodulation/equality.mli\ + paramodulation/inference.mli\ + paramodulation/equality_indexing.mli\ + paramodulation/indexing.mli \ + paramodulation/saturation.mli \ variousTactics.mli \ introductionTactics.mli eliminationTactics.mli negationTactics.mli \ - equalityTactics.mli autoTactic.mli discriminationTactics.mli inversion.mli \ - inversion_principle.mli ring.mli \ + equalityTactics.mli autoTactic.mli discriminationTactics.mli \ + inversion.mli inversion_principle.mli ring.mli setoids.mli \ fourier.mli fourierR.mli fwdSimplTactic.mli history.mli \ - statefulProofEngine.mli tactics.mli + statefulProofEngine.mli tactics.mli declarative.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)