added sqlStatements module (contains all CREATE TABLE/INDEX)

diff --git a/helm/ocaml/cic/.depend b/helm/ocaml/cic/.depend
index 21bc8d14afeeb19280e09a918769592917dd00bc..8d735abd3a17252a5ea33fc563bcf3a1ebf2e4e0 100644 (file)
--- 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 9e8bfadb7b7667eea0777c603d7f01fa9ff23c70..2074968ba839a04d4d404faf616e4798817fe531 100644 (file)
--- 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 5699c21840d1bb562aa163f57fb1d144ae8b2c75..bf364009e3d3e3fe7d9ee4c55d7097054660e95a 100644 (file)
--- 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 820add841dc7b55b383bc1f14163acb24296d003..0dc5572a0dd8f8ef7c01cc128890b95dce7c6a8e 100644 (file)
--- 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 f7a04516b70ed9deef39934dbec896e6c0a36c55..186c81793339f68909c23ddbdfb35dfbcf87a5b4 100644 (file)
--- 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 48a53815c59c73fb99970ab53640e245193d79de..04197957bc992225bd8cb7238bfc785585ef76bf 100644 (file)
--- 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 9d16a2c8da4eee6bf1529f273fd2c63f76e51d50..52fe27edd79b0e40ebab812bcf6b31c4723237f8 100644 (file)
--- 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 (file)
index 0000000..b57c661
--- /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 (file)
index 0000000..caf1e03
--- /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 8e1412bbbba85b1107e80e7cd39b284e19698158..2c6ce4b0f0813c89beb5db925b4e669698231435 100644 (file)
--- 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