From: Claudio Sacerdoti Coen Date: Thu, 22 Apr 2004 09:11:16 +0000 (+0000) Subject: IMPLEMENTATION_FILES now generated from INTERFACE_FILES. X-Git-Tag: dead_dir_walking~15 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=2041eed3f4385453291ae65c90e3011795a8b5bb IMPLEMENTATION_FILES now generated from INTERFACE_FILES. --- 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