Major changes to auto, documented on the helm mailing list.

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

diff --git a/components/tactics/paramodulation/indexing.mli b/components/tactics/paramodulation/indexing.mli
index e180511a64cbbd9f6d84d779249e83833b6ef615..340a1eddbc0acf0369ec36b29036d876a295a951 100644 (file)
--- 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 ->