X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Findexing.mli;h=06d1ada3fc795e055762f6937b3b6df61558e395;hb=b91d9e60b0a5f450d2725d4b9bb3ed7f81ef6d3a;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..06d1ada3f 100644
--- 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 ->