many changes:

[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 340a1eddbc0acf0369ec36b29036d876a295a951..7f464d2485af2c7f0b034172073e205bf1f5ee73 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.mli
+++ b/helm/software/components/tactics/paramodulation/indexing.mli
@@ -99,6 +99,14 @@ val check_target:
   Equality.equality_bag ->
   Cic.context ->
     Equality.equality -> string -> unit
+val solve_demodulating: 
+  Equality.equality_bag ->
+  Cic.metasenv * Cic.context * CicUniv.universe_graph ->
+  Index.t ->
+  Equality.goal ->
+  int ->
+    Equality.goal option
+
 
     (** profiling *)
 val get_stats: unit -> string