All the declarative tactics now have a more or less bugged implementation.

[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 7caaa78f47974b9d8b5f01b0d0d71d3c85ec532b..836a267dea78fa0f57cb0d8eb883d5f9e0c96f29 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.mli
+++ b/helm/software/components/tactics/paramodulation/indexing.mli
@@ -25,8 +25,6 @@
 
 (* $Id$ *)
 
-type goal = Equality.goal_proof * Cic.metasenv * Cic.term
-
 module Index :
   sig
     module PosEqSet : Set.S 
@@ -51,11 +49,11 @@ val subsumption :
   Index.t ->
   Equality.equality ->
   (Subst.substitution * Equality.equality * bool) option
+
 val superposition_left :
   Cic.conjecture list * Cic.context * CicUniv.universe_graph ->
-  Index.t ->
-  goal ->
-   goal list
+  Index.t -> Equality.goal -> int ->
+    int * Equality.goal list
 
 val superposition_right :
   ?subterms_only:bool ->
@@ -72,12 +70,12 @@ val demodulation_equality :
   int ->
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
   Index.t ->
-  Utils.equality_sign -> Equality.equality -> int * Equality.equality
+  Equality.equality -> int * Equality.equality
 val demodulation_goal :
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
   Index.t ->
-  goal ->
-  bool * goal
+  Equality.goal ->
+  bool * Equality.goal
 val demodulation_theorem :
   'a ->
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->