New tactics ncut and nlapply.

[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 8370d9da31238f0dadff13b0b7162fa3482f7697..06d1ada3fc795e055762f6937b3b6df61558e395 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.mli
+++ b/helm/software/components/tactics/paramodulation/indexing.mli
@@ -31,7 +31,7 @@ module Index :
       with type elt = Utils.pos * Equality.equality
       and type t = Equality_indexing.DT.PosEqSet.t
     type t =
-            Discrimination_tree.Make(Discrimination_tree.CicIndexable)(PosEqSet).t
+            Discrimination_tree.Make(Cic_indexable.CicIndexable)(PosEqSet).t
   end
 
 val check_for_duplicates : Cic.metasenv -> string -> unit
@@ -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 ->