From f55b5800229c0819448abf38dfeb1527b4ec08e2 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 21 Oct 2004 08:14:40 +0000 Subject: [PATCH] added reference to MetadataQuery (now it builds properly) --- helm/ocaml/tactics/.depend | 2 ++ helm/ocaml/tactics/Makefile | 6 ++++-- 2 files changed, 6 insertions(+), 2 deletions(-) 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 -- 2.39.2