update in delayed_updating

[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 8895b89a0dd671a4ce34577fe6d0cca2bd189081..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 ->
@@ -111,8 +117,6 @@ val solve_demodulating:
   Index.t ->
   Equality.goal ->
   int ->
-    Equality.goal option
-
+    (Equality.equality_bag * Equality.goal_proof * Cic.metasenv * 
+      Subst.substitution * Equality.proof) option
 
-    (** profiling *)
-val get_stats: unit -> string