From: Stefano Zacchiroli Date: Thu, 21 Oct 2004 08:14:40 +0000 (+0000) Subject: added reference to MetadataQuery (now it builds properly) X-Git-Tag: V_0_0_10~59 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f55b5800229c0819448abf38dfeb1527b4ec08e2;p=helm.git added reference to MetadataQuery (now it builds properly) --- diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend index 972c7071c..6f9e70476 100644 --- a/helm/ocaml/tactics/.depend +++ b/helm/ocaml/tactics/.depend @@ -42,6 +42,8 @@ primitiveTactics.cmo: proofEngineHelpers.cmi proofEngineReduction.cmi \ primitiveTactics.cmx: proofEngineHelpers.cmx proofEngineReduction.cmx \ proofEngineTypes.cmx reductionTactics.cmx tacticals.cmx \ primitiveTactics.cmi +metadataQuery.cmo: metadataQuery.cmi +metadataQuery.cmx: metadataQuery.cmi tacticChaser.cmo: filter_auto.cmi match_concl.cmi newConstraints.cmi \ primitiveTactics.cmi proofEngineTypes.cmi tacticChaser.cmi tacticChaser.cmx: filter_auto.cmx match_concl.cmx newConstraints.cmx \ diff --git a/helm/ocaml/tactics/Makefile b/helm/ocaml/tactics/Makefile index 2a4e59872..65b42b301 100644 --- a/helm/ocaml/tactics/Makefile +++ b/helm/ocaml/tactics/Makefile @@ -1,13 +1,15 @@ PACKAGE = tactics REQUIRES = \ pcre helm-cic_textual_parser helm-cic_proof_checking \ - helm-cic_unification helm-mathql_interpreter helm-mathql_generator + helm-cic_unification helm-mathql_interpreter helm-mathql_generator \ + dbi helm-metadata INTERFACE_FILES = \ proofEngineTypes.mli newConstraints.mli match_concl.mli filter_auto.mli\ proofEngineReduction.mli proofEngineHelpers.mli \ tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \ - primitiveTactics.mli tacticChaser.mli variousTactics.mli \ + primitiveTactics.mli metadataQuery.mli tacticChaser.mli \ + variousTactics.mli \ introductionTactics.mli eliminationTactics.mli negationTactics.mli \ equalityTactics.mli discriminationTactics.mli ring.mli fourier.mli \ fourierR.mli history.mli statefulProofEngine.mli