X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Finference.mli;h=5c6a1979b5c4a38c0ebe3c6dab3d8ae181c59fac;hb=ce800b0b7acf3940cad3afc5b1d2296155affb1c;hp=08d1c8f266010354deb9c48dbcf86d9c16fc7c1d;hpb=ba2372bd35aec412f5a7b61e5431236505567c43;p=helm.git

diff --git a/components/tactics/paramodulation/inference.mli b/components/tactics/paramodulation/inference.mli
index 08d1c8f26..5c6a1979b 100644
--- a/components/tactics/paramodulation/inference.mli
+++ b/components/tactics/paramodulation/inference.mli
@@ -30,7 +30,7 @@ val matching:
   Cic.metasenv -> Cic.metasenv -> Cic.context -> 
   Cic.term -> Cic.term ->
   CicUniv.universe_graph ->
-    Equality.substitution * Cic.metasenv * CicUniv.universe_graph
+    Subst.substitution * Cic.metasenv * CicUniv.universe_graph
 
 (**
    special unification that checks if the two terms are "simple", and in
@@ -40,7 +40,7 @@ val unification:
   Cic.metasenv -> Cic.metasenv -> Cic.context -> 
   Cic.term -> Cic.term ->
   CicUniv.universe_graph ->
-    Equality.substitution * Cic.metasenv * CicUniv.universe_graph
+    Subst.substitution * Cic.metasenv * CicUniv.universe_graph
 
     
 (**
@@ -57,7 +57,7 @@ val find_equalities:
    searches the library for equalities that can be applied to the current goal
 *)
 val find_library_equalities:
-  HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int ->
+  bool -> HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int ->
     UriManager.UriSet.t * (UriManager.uri * Equality.equality) list * int
 
 (**
@@ -75,3 +75,4 @@ val find_library_theorems:
 val find_context_hypotheses:
   Utils.environment -> int list -> (Cic.term * Cic.term * Cic.metasenv) list
 
+val get_stats: unit -> string