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=8370d9da31238f0dadff13b0b7162fa3482f7697;hpb=dcef667a444aa0f189225855c1433d26b65fb8b7;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/indexing.mli b/helm/software/components/tactics/paramodulation/indexing.mli
index 8370d9da3..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 ->