X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Findexing.mli;h=e36cfba494bbb432c77a8bb2185b73f72fdd5c35;hb=a3ee89dab26307ce1cedc8041ede995a97d51446;hp=8895b89a0dd671a4ce34577fe6d0cca2bd189081;hpb=7cb22a7f8107a6cde0b77b7879e04f586a347102;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/indexing.mli b/helm/software/components/tactics/paramodulation/indexing.mli
index 8895b89a0..e36cfba49 100644
--- a/helm/software/components/tactics/paramodulation/indexing.mli
+++ b/helm/software/components/tactics/paramodulation/indexing.mli
@@ -94,6 +94,12 @@ val demodulation_goal :
   Index.t ->
   Equality.goal ->
   bool * Equality.goal
+val demodulation_all_goal :
+  Equality.equality_bag ->
+  Cic.metasenv * Cic.context * CicUniv.universe_graph ->
+  Index.t ->
+  Equality.goal -> int ->
+    Equality.goal list
 val demodulation_theorem :
   Equality.equality_bag ->
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
@@ -111,8 +117,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