Added the computation of max_weight for equations in proofs.

[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 8fd6187024cbc9bc51ee579215de33480509aaff..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 
@@ -45,20 +43,21 @@ val unification :
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
   Index.t ->
   Equality.equality ->
-  (Subst.substitution * Equality.equality * Utils.pos) option
+  (Subst.substitution * Equality.equality * bool) option
 val subsumption :
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
   Index.t ->
   Equality.equality ->
-  (Subst.substitution * Equality.equality * Utils.pos) option
+  (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 ->
+    UriManager.uri ->
   int ->
   'a * Cic.context * CicUniv.universe_graph ->
   Index.t ->
@@ -67,15 +66,16 @@ val superposition_right :
 
 val demodulation_equality :
   ?from:string -> 
+  UriManager.uri ->
   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 ->