From 2041eed3f4385453291ae65c90e3011795a8b5bb Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 22 Apr 2004 09:11:16 +0000 Subject: [PATCH] IMPLEMENTATION_FILES now generated from INTERFACE_FILES. --- helm/ocaml/tactics/Makefile | 23 ++++++++--------------- 1 file changed, 8 insertions(+), 15 deletions(-) diff --git a/helm/ocaml/tactics/Makefile b/helm/ocaml/tactics/Makefile index 4436c2142..ddd001cd1 100644 --- a/helm/ocaml/tactics/Makefile +++ b/helm/ocaml/tactics/Makefile @@ -1,22 +1,15 @@ PACKAGE = tactics REQUIRES = \ - pcre \ - helm-cic_textual_parser helm-cic_proof_checking helm-cic_unification \ - helm-mathql_interpreter helm-mathql_generator + pcre helm-cic_textual_parser helm-cic_proof_checking \ + helm-cic_unification helm-mathql_interpreter helm-mathql_generator -INTERFACE_FILES = \ +INTERFACE_FILES = \ proofEngineReduction.mli proofEngineHelpers.mli \ - tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \ - primitiveTactics.mli tacticChaser.mli variousTactics.mli introductionTactics.mli \ - eliminationTactics.mli negationTactics.mli equalityTactics.mli \ - discriminationTactics.mli ring.mli fourierR.mli -IMPLEMENTATION_FILES = \ - proofEngineTypes.ml proofEngineReduction.ml proofEngineHelpers.ml \ - fourier.ml tacticals.ml reductionTactics.ml proofEngineStructuralRules.ml \ - primitiveTactics.ml tacticChaser.ml variousTactics.ml introductionTactics.ml \ - eliminationTactics.ml negationTactics.ml equalityTactics.ml \ - discriminationTactics.ml ring.ml fourierR.ml - + tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \ + primitiveTactics.mli tacticChaser.mli variousTactics.mli \ + introductionTactics.mli eliminationTactics.mli negationTactics.mli \ + equalityTactics.mli discriminationTactics.mli ring.mli fourierR.mli +IMPLEMENTATION_FILES = proofEngineTypes.ml $(INTERFACE_FILES:%.mli=%.ml) include ../Makefile.common -- 2.39.2