From a268d7377c1d4ddae4229f5844125f827325c78a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 3 May 2005 13:38:25 +0000 Subject: [PATCH] added sqlStatements module (contains all CREATE TABLE/INDEX) --- helm/ocaml/cic/.depend | 18 ++-- helm/ocaml/cic_omdoc/.depend | 10 +- helm/ocaml/cic_unification/.depend | 12 +-- helm/ocaml/mathql_generator/.depend | 8 +- helm/ocaml/mathql_interpreter/.depend | 20 ++-- helm/ocaml/metadata/.depend | 3 + helm/ocaml/metadata/Makefile | 17 +++- helm/ocaml/metadata/sqlStatements.ml | 105 +++++++++++++++++++++ helm/ocaml/metadata/sqlStatements.mli | 7 ++ helm/ocaml/tactics/.depend | 130 +++++++++++++------------- 10 files changed, 228 insertions(+), 102 deletions(-) create mode 100644 helm/ocaml/metadata/sqlStatements.ml create mode 100644 helm/ocaml/metadata/sqlStatements.mli diff --git a/helm/ocaml/cic/.depend b/helm/ocaml/cic/.depend index 21bc8d14a..8d735abd3 100644 --- a/helm/ocaml/cic/.depend +++ b/helm/ocaml/cic/.depend @@ -1,6 +1,6 @@ deannotate.cmi: cic.cmo cicParser3.cmi: cic.cmo -cicParser2.cmi: cic.cmo cicParser3.cmi +cicParser2.cmi: cicParser3.cmi cic.cmo cicParser.cmi: cic.cmo cicUtil.cmi: cic.cmo helmLibraryObjects.cmi: cic.cmo @@ -10,13 +10,13 @@ cicUniv.cmo: cicUniv.cmi cicUniv.cmx: cicUniv.cmi deannotate.cmo: cic.cmo deannotate.cmi deannotate.cmx: cic.cmx deannotate.cmi -cicParser3.cmo: cic.cmo cicUniv.cmi cicParser3.cmi -cicParser3.cmx: cic.cmx cicUniv.cmx cicParser3.cmi -cicParser2.cmo: cic.cmo cicParser3.cmi cicParser2.cmi -cicParser2.cmx: cic.cmx cicParser3.cmx cicParser2.cmi -cicParser.cmo: cicParser2.cmi cicParser3.cmi deannotate.cmi cicParser.cmi -cicParser.cmx: cicParser2.cmx cicParser3.cmx deannotate.cmx cicParser.cmi -cicUtil.cmo: cic.cmo cicUtil.cmi -cicUtil.cmx: cic.cmx cicUtil.cmi +cicParser3.cmo: cicUniv.cmi cic.cmo cicParser3.cmi +cicParser3.cmx: cicUniv.cmx cic.cmx cicParser3.cmi +cicParser2.cmo: cicParser3.cmi cic.cmo cicParser2.cmi +cicParser2.cmx: cicParser3.cmx cic.cmx cicParser2.cmi +cicParser.cmo: deannotate.cmi cicParser3.cmi cicParser2.cmi cicParser.cmi +cicParser.cmx: deannotate.cmx cicParser3.cmx cicParser2.cmx cicParser.cmi +cicUtil.cmo: cicUniv.cmi cic.cmo cicUtil.cmi +cicUtil.cmx: cicUniv.cmx cic.cmx cicUtil.cmi helmLibraryObjects.cmo: cic.cmo helmLibraryObjects.cmi helmLibraryObjects.cmx: cic.cmx helmLibraryObjects.cmi diff --git a/helm/ocaml/cic_omdoc/.depend b/helm/ocaml/cic_omdoc/.depend index 9e8bfadb7..2074968ba 100644 --- a/helm/ocaml/cic_omdoc/.depend +++ b/helm/ocaml/cic_omdoc/.depend @@ -1,17 +1,17 @@ contentPp.cmi: content.cmi -cic2content.cmi: cic2acic.cmi content.cmi +cic2content.cmi: content.cmi cic2acic.cmi content2cic.cmi: content.cmi eta_fixing.cmo: eta_fixing.cmi eta_fixing.cmx: eta_fixing.cmi doubleTypeInference.cmo: doubleTypeInference.cmi doubleTypeInference.cmx: doubleTypeInference.cmi -cic2acic.cmo: doubleTypeInference.cmi eta_fixing.cmi cic2acic.cmi -cic2acic.cmx: doubleTypeInference.cmx eta_fixing.cmx cic2acic.cmi +cic2acic.cmo: eta_fixing.cmi doubleTypeInference.cmi cic2acic.cmi +cic2acic.cmx: eta_fixing.cmx doubleTypeInference.cmx cic2acic.cmi content.cmo: content.cmi content.cmx: content.cmi contentPp.cmo: content.cmi contentPp.cmi contentPp.cmx: content.cmx contentPp.cmi -cic2content.cmo: cic2acic.cmi content.cmi cic2content.cmi -cic2content.cmx: cic2acic.cmx content.cmx cic2content.cmi +cic2content.cmo: content.cmi cic2acic.cmi cic2content.cmi +cic2content.cmx: content.cmx cic2acic.cmx cic2content.cmi content2cic.cmo: content.cmi content2cic.cmi content2cic.cmx: content.cmx content2cic.cmi diff --git a/helm/ocaml/cic_unification/.depend b/helm/ocaml/cic_unification/.depend index 5699c2184..bf364009e 100644 --- a/helm/ocaml/cic_unification/.depend +++ b/helm/ocaml/cic_unification/.depend @@ -4,13 +4,13 @@ cicMkImplicit.cmo: cicMkImplicit.cmi cicMkImplicit.cmx: cicMkImplicit.cmi freshNamesGenerator.cmo: freshNamesGenerator.cmi freshNamesGenerator.cmx: freshNamesGenerator.cmi -cicUnification.cmo: cicMetaSubst.cmi freshNamesGenerator.cmi \ +cicUnification.cmo: freshNamesGenerator.cmi cicMetaSubst.cmi \ cicUnification.cmi -cicUnification.cmx: cicMetaSubst.cmx freshNamesGenerator.cmx \ +cicUnification.cmx: freshNamesGenerator.cmx cicMetaSubst.cmx \ cicUnification.cmi coercGraph.cmo: freshNamesGenerator.cmi coercGraph.cmi coercGraph.cmx: freshNamesGenerator.cmx coercGraph.cmi -cicRefine.cmo: cicMetaSubst.cmi cicMkImplicit.cmi cicUnification.cmi \ - freshNamesGenerator.cmi cicRefine.cmi -cicRefine.cmx: cicMetaSubst.cmx cicMkImplicit.cmx cicUnification.cmx \ - freshNamesGenerator.cmx cicRefine.cmi +cicRefine.cmo: freshNamesGenerator.cmi cicUnification.cmi cicMkImplicit.cmi \ + cicMetaSubst.cmi cicRefine.cmi +cicRefine.cmx: freshNamesGenerator.cmx cicUnification.cmx cicMkImplicit.cmx \ + cicMetaSubst.cmx cicRefine.cmi diff --git a/helm/ocaml/mathql_generator/.depend b/helm/ocaml/mathql_generator/.depend index 820add841..0dc5572a0 100644 --- a/helm/ocaml/mathql_generator/.depend +++ b/helm/ocaml/mathql_generator/.depend @@ -5,11 +5,11 @@ cGSearchPattern.cmi: mQGTypes.cmo cGLocateInductive.cmi: mQGTypes.cmo mQGUtil.cmo: mQGTypes.cmo mQGUtil.cmi mQGUtil.cmx: mQGTypes.cmx mQGUtil.cmi -mQueryGenerator.cmo: mQGTypes.cmo mQGUtil.cmi mQueryGenerator.cmi -mQueryGenerator.cmx: mQGTypes.cmx mQGUtil.cmx mQueryGenerator.cmi +mQueryGenerator.cmo: mQGUtil.cmi mQGTypes.cmo mQueryGenerator.cmi +mQueryGenerator.cmx: mQGUtil.cmx mQGTypes.cmx mQueryGenerator.cmi cGMatchConclusion.cmo: mQGTypes.cmo cGMatchConclusion.cmi cGMatchConclusion.cmx: mQGTypes.cmx cGMatchConclusion.cmi -cGSearchPattern.cmo: mQGTypes.cmo mQGUtil.cmi cGSearchPattern.cmi -cGSearchPattern.cmx: mQGTypes.cmx mQGUtil.cmx cGSearchPattern.cmi +cGSearchPattern.cmo: mQGUtil.cmi mQGTypes.cmo cGSearchPattern.cmi +cGSearchPattern.cmx: mQGUtil.cmx mQGTypes.cmx cGSearchPattern.cmi cGLocateInductive.cmo: mQGTypes.cmo cGLocateInductive.cmi cGLocateInductive.cmx: mQGTypes.cmx cGLocateInductive.cmi diff --git a/helm/ocaml/mathql_interpreter/.depend b/helm/ocaml/mathql_interpreter/.depend index f7a04516b..186c81793 100644 --- a/helm/ocaml/mathql_interpreter/.depend +++ b/helm/ocaml/mathql_interpreter/.depend @@ -1,14 +1,14 @@ mQIPostgres.cmi: mQITypes.cmo mQIMySql.cmi: mQITypes.cmo -mQIConn.cmi: mQIMap.cmi mQITypes.cmo -mQIProperty.cmi: mQIConn.cmi mQITypes.cmo +mQIConn.cmi: mQITypes.cmo mQIMap.cmi +mQIProperty.cmi: mQITypes.cmo mQIConn.cmi mQueryInterpreter.cmi: mQIConn.cmi mQueryTParser.cmo: mQueryTParser.cmi mQueryTParser.cmx: mQueryTParser.cmi mQueryTLexer.cmo: mQueryTParser.cmi mQueryTLexer.cmx: mQueryTParser.cmx -mQueryUtil.cmo: mQueryTLexer.cmo mQueryTParser.cmi mQueryUtil.cmi -mQueryUtil.cmx: mQueryTLexer.cmx mQueryTParser.cmx mQueryUtil.cmi +mQueryUtil.cmo: mQueryTParser.cmi mQueryTLexer.cmo mQueryUtil.cmi +mQueryUtil.cmx: mQueryTParser.cmx mQueryTLexer.cmx mQueryUtil.cmi mQIUtil.cmo: mQIUtil.cmi mQIUtil.cmx: mQIUtil.cmi mQIPostgres.cmo: mQIPostgres.cmi @@ -17,11 +17,11 @@ mQIMySql.cmo: mQIMySql.cmi mQIMySql.cmx: mQIMySql.cmi mQIMap.cmo: mQueryUtil.cmi mQIMap.cmi mQIMap.cmx: mQueryUtil.cmx mQIMap.cmi -mQIConn.cmo: mQIMap.cmi mQIMySql.cmi mQIPostgres.cmi mQIConn.cmi -mQIConn.cmx: mQIMap.cmx mQIMySql.cmx mQIPostgres.cmx mQIConn.cmi -mQIProperty.cmo: mQIConn.cmi mQIMap.cmi mQIUtil.cmi mQIProperty.cmi -mQIProperty.cmx: mQIConn.cmx mQIMap.cmx mQIUtil.cmx mQIProperty.cmi -mQueryInterpreter.cmo: mQIConn.cmi mQIProperty.cmi mQIUtil.cmi mQueryUtil.cmi \ +mQIConn.cmo: mQIPostgres.cmi mQIMySql.cmi mQIMap.cmi mQIConn.cmi +mQIConn.cmx: mQIPostgres.cmx mQIMySql.cmx mQIMap.cmx mQIConn.cmi +mQIProperty.cmo: mQIUtil.cmi mQIMap.cmi mQIConn.cmi mQIProperty.cmi +mQIProperty.cmx: mQIUtil.cmx mQIMap.cmx mQIConn.cmx mQIProperty.cmi +mQueryInterpreter.cmo: mQueryUtil.cmi mQIUtil.cmi mQIProperty.cmi mQIConn.cmi \ mQueryInterpreter.cmi -mQueryInterpreter.cmx: mQIConn.cmx mQIProperty.cmx mQIUtil.cmx mQueryUtil.cmx \ +mQueryInterpreter.cmx: mQueryUtil.cmx mQIUtil.cmx mQIProperty.cmx mQIConn.cmx \ mQueryInterpreter.cmi diff --git a/helm/ocaml/metadata/.depend b/helm/ocaml/metadata/.depend index 48a53815c..04197957b 100644 --- a/helm/ocaml/metadata/.depend +++ b/helm/ocaml/metadata/.depend @@ -1,6 +1,9 @@ metadataExtractor.cmi: metadataTypes.cmi metadataPp.cmi: metadataTypes.cmi metadataConstraints.cmi: metadataTypes.cmi +metadataDb.cmi: metadataTypes.cmi +sqlStatements.cmo: sqlStatements.cmi +sqlStatements.cmx: sqlStatements.cmi metadataTypes.cmo: metadataTypes.cmi metadataTypes.cmx: metadataTypes.cmi metadataExtractor.cmo: metadataTypes.cmi metadataExtractor.cmi diff --git a/helm/ocaml/metadata/Makefile b/helm/ocaml/metadata/Makefile index 9d16a2c8d..52fe27edd 100644 --- a/helm/ocaml/metadata/Makefile +++ b/helm/ocaml/metadata/Makefile @@ -3,6 +3,7 @@ REQUIRES = mysql helm-cic_proof_checking PREDICATES = INTERFACE_FILES = \ + sqlStatements.mli \ metadataTypes.mli \ metadataExtractor.mli \ metadataPp.mli \ @@ -12,8 +13,21 @@ IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = -all: +include ../Makefile.common + +all: all_table_creator +opt: opt_table_creator + +all_table_creator: + make -C table_creator/ all +opt_table_creator: + make -C table_creator/ opt +clean: clean_table_creator + +clean_table_creator: + make -C table_creator/ clean + test: test.ml $(PACKAGE).cma $(OCAMLFIND) ocamlc -thread -package mysql,helm-metadata -linkpkg -o $@ $< test.opt: test.ml $(PACKAGE).cmxa @@ -21,4 +35,3 @@ test.opt: test.ml $(PACKAGE).cmxa test_query: test_query.ml $(PACKAGE).cma $(OCAMLFIND) ocamlc -thread -package mysql,helm-metadata -linkpkg -o $@ $< -include ../Makefile.common diff --git a/helm/ocaml/metadata/sqlStatements.ml b/helm/ocaml/metadata/sqlStatements.ml new file mode 100644 index 000000000..b57c661f3 --- /dev/null +++ b/helm/ocaml/metadata/sqlStatements.ml @@ -0,0 +1,105 @@ + +open Printf;; +type tbl = [ `RefObj| `RefSort| `RefRel| `ObjectName| `Owners| `Count] + +(* TABLES *) + +let sprintf_refObj_format name = sprintf " +CREATE TABLE %s ( + source varchar(255) binary not null, + h_occurrence varchar(255) binary not null, + h_position varchar(255) binary not null, + h_depth integer +);" name + +let sprintf_refSort_format name = sprintf " +CREATE TABLE %s ( + source varchar(255) binary not null, + h_position varchar(255) binary not null, + h_depth integer not null, + h_sort varchar(255) binary not null +);" name + +let sprintf_refRel_format name = sprintf " +CREATE TABLE %s ( + source varchar(255) binary not null, + h_position varchar(255) binary not null, + h_depth integer not null +);" name + +let sprintf_objectName_format name = sprintf " +CREATE TABLE %s ( + source varchar(255) binary not null, + value varchar(255) binary not null +);" name + +let sprintf_owners_format name = sprintf " +CREATE TABLE %s ( + source varchar(255) binary not null, + owner varchar(255) binary not null +);" name + +let sprintf_count_format name = sprintf " +CREATE TABLE %s ( + source varchar(255) binary unique not null, + conclusion smallint(6) not null, + hypothesis smallint(6) not null, + statement smallint(6) not null +);" name + +(* INDEXES *) + +let sprintf_refObj_index name = sprintf " +CREATE INDEX %s_source ON %s (source); +CREATE INDEX %s_target ON %s (h_occurrence); +CREATE INDEX %s_position ON %s (h_position); +" name name name name name name + +let sprintf_refSort_index name = sprintf " +CREATE INDEX %s_source ON %s (source); +" name name + +let sprintf_objectName_index name = sprintf " +CREATE INDEX %s_value ON %s (value); +" name name + +let sprintf_owners_index name = sprintf " +CREATE INDEX %s_owner ON %s (owner); +CREATE INDEX %s_source ON %s (source); +" name name name name + +let sprintf_count_index name = sprintf " +CREATE INDEX %s_source ON %s (source); +CREATE INDEX %s_conclusion ON %s (conclusion); +CREATE INDEX %s_hypothesis ON %s (hypothesis); +CREATE INDEX %s_statement ON %s (statement); +" name name name name name name name name + +let sprintf_refRel_index name = "" + +(* FUNCTIONS *) + +let get_table_format t named = + match t with + | `RefObj -> sprintf_refObj_format named + | `RefSort -> sprintf_refSort_format named + | `RefRel -> sprintf_refRel_format named + | `ObjectName -> sprintf_objectName_format named + | `Owners -> sprintf_owners_format named + | `Count -> sprintf_count_format named + +let get_index_format t named = + match t with + | `RefObj -> sprintf_refObj_index named + | `RefSort -> sprintf_refSort_index named + | `RefRel -> sprintf_refRel_index named + | `ObjectName -> sprintf_objectName_index named + | `Owners -> sprintf_owners_index named + | `Count -> sprintf_count_index named + +let create_tables l = + List.fold_left (fun s (name,table) -> s ^ get_table_format table name) "" l + +let create_indexes l = + List.fold_left (fun s (name,table) -> s ^ get_index_format table name) "" l + diff --git a/helm/ocaml/metadata/sqlStatements.mli b/helm/ocaml/metadata/sqlStatements.mli new file mode 100644 index 000000000..caf1e037b --- /dev/null +++ b/helm/ocaml/metadata/sqlStatements.mli @@ -0,0 +1,7 @@ + +type tbl = [ `RefObj| `RefSort| `RefRel| `ObjectName| `Owners| `Count] + +val create_tables: (string * tbl) list -> string + +val create_indexes: (string * tbl) list -> string + diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend index 8e1412bbb..2c6ce4b0f 100644 --- a/helm/ocaml/tactics/.depend +++ b/helm/ocaml/tactics/.depend @@ -23,85 +23,83 @@ proofEngineHelpers.cmo: proofEngineHelpers.cmi proofEngineHelpers.cmx: proofEngineHelpers.cmi tacticals.cmo: proofEngineTypes.cmi tacticals.cmi tacticals.cmx: proofEngineTypes.cmx tacticals.cmi -reductionTactics.cmo: proofEngineReduction.cmi proofEngineTypes.cmi \ +reductionTactics.cmo: proofEngineTypes.cmi proofEngineReduction.cmi \ reductionTactics.cmi -reductionTactics.cmx: proofEngineReduction.cmx proofEngineTypes.cmx \ +reductionTactics.cmx: proofEngineTypes.cmx proofEngineReduction.cmx \ reductionTactics.cmi proofEngineStructuralRules.cmo: proofEngineTypes.cmi \ proofEngineStructuralRules.cmi proofEngineStructuralRules.cmx: proofEngineTypes.cmx \ proofEngineStructuralRules.cmi -primitiveTactics.cmo: proofEngineHelpers.cmi proofEngineReduction.cmi \ - proofEngineTypes.cmi reductionTactics.cmi tacticals.cmi \ - primitiveTactics.cmi -primitiveTactics.cmx: proofEngineHelpers.cmx proofEngineReduction.cmx \ - proofEngineTypes.cmx reductionTactics.cmx tacticals.cmx \ - primitiveTactics.cmi +primitiveTactics.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \ + proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi +primitiveTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \ + proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmi hashtbl_equiv.cmo: hashtbl_equiv.cmi hashtbl_equiv.cmx: hashtbl_equiv.cmi -metadataQuery.cmo: hashtbl_equiv.cmi primitiveTactics.cmi \ - proofEngineTypes.cmi metadataQuery.cmi -metadataQuery.cmx: hashtbl_equiv.cmx primitiveTactics.cmx \ - proofEngineTypes.cmx metadataQuery.cmi -variousTactics.cmo: primitiveTactics.cmi proofEngineReduction.cmi \ - proofEngineTypes.cmi tacticals.cmi variousTactics.cmi -variousTactics.cmx: primitiveTactics.cmx proofEngineReduction.cmx \ - proofEngineTypes.cmx tacticals.cmx variousTactics.cmi -autoTactic.cmo: metadataQuery.cmi primitiveTactics.cmi proofEngineHelpers.cmi \ - proofEngineTypes.cmi autoTactic.cmi -autoTactic.cmx: metadataQuery.cmx primitiveTactics.cmx proofEngineHelpers.cmx \ - proofEngineTypes.cmx autoTactic.cmi -introductionTactics.cmo: primitiveTactics.cmi proofEngineTypes.cmi \ +metadataQuery.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ + hashtbl_equiv.cmi metadataQuery.cmi +metadataQuery.cmx: proofEngineTypes.cmx primitiveTactics.cmx \ + hashtbl_equiv.cmx metadataQuery.cmi +variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \ + proofEngineReduction.cmi primitiveTactics.cmi variousTactics.cmi +variousTactics.cmx: tacticals.cmx proofEngineTypes.cmx \ + proofEngineReduction.cmx primitiveTactics.cmx variousTactics.cmi +autoTactic.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi \ + primitiveTactics.cmi metadataQuery.cmi autoTactic.cmi +autoTactic.cmx: proofEngineTypes.cmx proofEngineHelpers.cmx \ + primitiveTactics.cmx metadataQuery.cmx autoTactic.cmi +introductionTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ introductionTactics.cmi -introductionTactics.cmx: primitiveTactics.cmx proofEngineTypes.cmx \ +introductionTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \ introductionTactics.cmi -eliminationTactics.cmo: primitiveTactics.cmi proofEngineStructuralRules.cmi \ - proofEngineTypes.cmi tacticals.cmi eliminationTactics.cmi -eliminationTactics.cmx: primitiveTactics.cmx proofEngineStructuralRules.cmx \ - proofEngineTypes.cmx tacticals.cmx eliminationTactics.cmi -negationTactics.cmo: eliminationTactics.cmi primitiveTactics.cmi \ - proofEngineTypes.cmi tacticals.cmi variousTactics.cmi negationTactics.cmi -negationTactics.cmx: eliminationTactics.cmx primitiveTactics.cmx \ - proofEngineTypes.cmx tacticals.cmx variousTactics.cmx negationTactics.cmi -equalityTactics.cmo: introductionTactics.cmi primitiveTactics.cmi \ - proofEngineHelpers.cmi proofEngineReduction.cmi \ - proofEngineStructuralRules.cmi proofEngineTypes.cmi reductionTactics.cmi \ - tacticals.cmi equalityTactics.cmi -equalityTactics.cmx: introductionTactics.cmx primitiveTactics.cmx \ - proofEngineHelpers.cmx proofEngineReduction.cmx \ - proofEngineStructuralRules.cmx proofEngineTypes.cmx reductionTactics.cmx \ - tacticals.cmx equalityTactics.cmi -discriminationTactics.cmo: eliminationTactics.cmi equalityTactics.cmi \ - introductionTactics.cmi primitiveTactics.cmi proofEngineTypes.cmi \ - tacticals.cmi discriminationTactics.cmi -discriminationTactics.cmx: eliminationTactics.cmx equalityTactics.cmx \ - introductionTactics.cmx primitiveTactics.cmx proofEngineTypes.cmx \ - tacticals.cmx discriminationTactics.cmi -ring.cmo: eliminationTactics.cmi equalityTactics.cmi primitiveTactics.cmi \ - proofEngineStructuralRules.cmi proofEngineTypes.cmi tacticals.cmi \ - ring.cmi -ring.cmx: eliminationTactics.cmx equalityTactics.cmx primitiveTactics.cmx \ - proofEngineStructuralRules.cmx proofEngineTypes.cmx tacticals.cmx \ - ring.cmi +eliminationTactics.cmo: tacticals.cmi proofEngineTypes.cmi \ + proofEngineStructuralRules.cmi primitiveTactics.cmi \ + eliminationTactics.cmi +eliminationTactics.cmx: tacticals.cmx proofEngineTypes.cmx \ + proofEngineStructuralRules.cmx primitiveTactics.cmx \ + eliminationTactics.cmi +negationTactics.cmo: variousTactics.cmi tacticals.cmi proofEngineTypes.cmi \ + primitiveTactics.cmi eliminationTactics.cmi negationTactics.cmi +negationTactics.cmx: variousTactics.cmx tacticals.cmx proofEngineTypes.cmx \ + primitiveTactics.cmx eliminationTactics.cmx negationTactics.cmi +equalityTactics.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \ + proofEngineStructuralRules.cmi proofEngineReduction.cmi \ + proofEngineHelpers.cmi primitiveTactics.cmi introductionTactics.cmi \ + equalityTactics.cmi +equalityTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \ + proofEngineStructuralRules.cmx proofEngineReduction.cmx \ + proofEngineHelpers.cmx primitiveTactics.cmx introductionTactics.cmx \ + equalityTactics.cmi +discriminationTactics.cmo: tacticals.cmi proofEngineTypes.cmi \ + primitiveTactics.cmi introductionTactics.cmi equalityTactics.cmi \ + eliminationTactics.cmi discriminationTactics.cmi +discriminationTactics.cmx: tacticals.cmx proofEngineTypes.cmx \ + primitiveTactics.cmx introductionTactics.cmx equalityTactics.cmx \ + eliminationTactics.cmx discriminationTactics.cmi +ring.cmo: tacticals.cmi proofEngineTypes.cmi proofEngineStructuralRules.cmi \ + primitiveTactics.cmi equalityTactics.cmi eliminationTactics.cmi ring.cmi +ring.cmx: tacticals.cmx proofEngineTypes.cmx proofEngineStructuralRules.cmx \ + primitiveTactics.cmx equalityTactics.cmx eliminationTactics.cmx ring.cmi fourier.cmo: fourier.cmi fourier.cmx: fourier.cmi -fourierR.cmo: equalityTactics.cmi fourier.cmi primitiveTactics.cmi \ - proofEngineHelpers.cmi proofEngineTypes.cmi reductionTactics.cmi ring.cmi \ - tacticals.cmi fourierR.cmi -fourierR.cmx: equalityTactics.cmx fourier.cmx primitiveTactics.cmx \ - proofEngineHelpers.cmx proofEngineTypes.cmx reductionTactics.cmx ring.cmx \ - tacticals.cmx fourierR.cmi +fourierR.cmo: tacticals.cmi ring.cmi reductionTactics.cmi \ + proofEngineTypes.cmi proofEngineHelpers.cmi primitiveTactics.cmi \ + fourier.cmi equalityTactics.cmi fourierR.cmi +fourierR.cmx: tacticals.cmx ring.cmx reductionTactics.cmx \ + proofEngineTypes.cmx proofEngineHelpers.cmx primitiveTactics.cmx \ + fourier.cmx equalityTactics.cmx fourierR.cmi history.cmo: history.cmi history.cmx: history.cmi -statefulProofEngine.cmo: history.cmi proofEngineTypes.cmi \ +statefulProofEngine.cmo: proofEngineTypes.cmi history.cmi \ statefulProofEngine.cmi -statefulProofEngine.cmx: history.cmx proofEngineTypes.cmx \ +statefulProofEngine.cmx: proofEngineTypes.cmx history.cmx \ statefulProofEngine.cmi -tactics.cmo: autoTactic.cmi discriminationTactics.cmi eliminationTactics.cmi \ - equalityTactics.cmi fourierR.cmi introductionTactics.cmi \ - negationTactics.cmi primitiveTactics.cmi reductionTactics.cmi ring.cmi \ - variousTactics.cmi tactics.cmi -tactics.cmx: autoTactic.cmx discriminationTactics.cmx eliminationTactics.cmx \ - equalityTactics.cmx fourierR.cmx introductionTactics.cmx \ - negationTactics.cmx primitiveTactics.cmx reductionTactics.cmx ring.cmx \ - variousTactics.cmx tactics.cmi +tactics.cmo: variousTactics.cmi ring.cmi reductionTactics.cmi \ + primitiveTactics.cmi negationTactics.cmi introductionTactics.cmi \ + fourierR.cmi equalityTactics.cmi eliminationTactics.cmi \ + discriminationTactics.cmi autoTactic.cmi tactics.cmi +tactics.cmx: variousTactics.cmx ring.cmx reductionTactics.cmx \ + primitiveTactics.cmx negationTactics.cmx introductionTactics.cmx \ + fourierR.cmx equalityTactics.cmx eliminationTactics.cmx \ + discriminationTactics.cmx autoTactic.cmx tactics.cmi -- 2.39.2