New demod function working for arbitary goals.

[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 9e7ba76f701d943c6a78039812c5e478e713dcf9..1caa5ed41b5b0b46946552800caf04c1fcaf6052 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.mli
+++ b/helm/software/components/tactics/paramodulation/indexing.mli
@@ -31,9 +31,10 @@ module Index :
       with type elt = Utils.pos * Equality.equality
       and type t = Equality_indexing.DT.PosEqSet.t
     type t =
-            Discrimination_tree.DiscriminationTreeIndexing(Discrimination_tree.CicIndexable)(PosEqSet).t
+            Discrimination_tree.Make(Discrimination_tree.CicIndexable)(PosEqSet).t
   end
 
+val check_for_duplicates : Cic.metasenv -> string -> unit
 val index : Index.t -> Equality.equality -> Index.t
 val remove_index : Index.t -> Equality.equality -> Index.t
 val in_index : Index.t -> Equality.equality -> bool
@@ -75,6 +76,12 @@ val superposition_right :
   Equality.equality ->
   int * Equality.equality list
 
+val demod :
+  Equality.equality_bag ->
+  Cic.metasenv * Cic.context * CicUniv.universe_graph ->
+  Index.t ->
+  Equality.goal ->
+  bool * Equality.goal
 val demodulation_equality :
   Equality.equality_bag ->
   ?from:string ->