huge commit in automation:

[helm.git] / helm / software / components / tactics / paramodulation / indexing.mli

diff --git a/helm/software/components/tactics/paramodulation/indexing.mli b/helm/software/components/tactics/paramodulation/indexing.mli
index 8895b89a0dd671a4ce34577fe6d0cca2bd189081..8370d9da31238f0dadff13b0b7162fa3482f7697 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.mli
+++ b/helm/software/components/tactics/paramodulation/indexing.mli
@@ -111,8 +111,6 @@ val solve_demodulating:
   Index.t ->
   Equality.goal ->
   int ->
-    Equality.goal option
+    (Equality.equality_bag * Equality.goal_proof * Cic.metasenv * 
+      Subst.substitution * Equality.proof) option
 
-
-    (** profiling *)
-val get_stats: unit -> string