X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Findexing.mli;h=340a1eddbc0acf0369ec36b29036d876a295a951;hb=f104e234238586ac846881feb30e1b56a509cfd3;hp=e180511a64cbbd9f6d84d779249e83833b6ef615;hpb=e3f6d410ebe780d1b26a0bcf982ef900a94e95a7;p=helm.git

diff --git a/components/tactics/paramodulation/indexing.mli b/components/tactics/paramodulation/indexing.mli
index e180511a6..340a1eddb 100644
--- a/components/tactics/paramodulation/indexing.mli
+++ b/components/tactics/paramodulation/indexing.mli
@@ -48,7 +48,16 @@ val subsumption :
   Index.t ->
   Equality.equality ->
   (Subst.substitution * Equality.equality * bool) option
-
+val unification_all :
+  Cic.metasenv * Cic.context * CicUniv.universe_graph ->
+  Index.t ->
+  Equality.equality ->
+  (Subst.substitution * Equality.equality * bool) list
+val subsumption_all :
+  Cic.metasenv * Cic.context * CicUniv.universe_graph ->
+  Index.t ->
+  Equality.equality ->
+  (Subst.substitution * Equality.equality * bool) list
 val superposition_left :
   Equality.equality_bag ->
   Cic.conjecture list * Cic.context * CicUniv.universe_graph ->