X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Fequality.mli;h=1a2a3a2808d3d284a4f00f4eda4ebe289f5b2ca5;hb=1a65db059b643422fc8eded4f4e03b512071515b;hp=4d48f22aade7a4aa888b99d924963731e918f3ce;hpb=d5950e1810f3a6d89328f18c2c5796e54a907473;p=helm.git

diff --git a/components/tactics/paramodulation/equality.mli b/components/tactics/paramodulation/equality.mli
index 4d48f22aa..1a2a3a280 100644
--- a/components/tactics/paramodulation/equality.mli
+++ b/components/tactics/paramodulation/equality.mli
@@ -45,7 +45,8 @@ and old_proof =
   | SubProof of Cic.term * int * old_proof
 
 and goal_proof = (Utils.pos * int * substitution * Cic.term) list
-	
+
+val pp_proof: (Cic.name option) list -> goal_proof -> new_proof -> string
 
 val empty_subst : substitution
 val apply_subst : substitution -> Cic.term -> Cic.term
@@ -69,6 +70,10 @@ val mk_equality :
   (Cic.term * Cic.term * Cic.term * Utils.comparison) *
   Cic.metasenv -> 
     equality
+
+val mk_tmp_equality :
+  int * (Cic.term * Cic.term * Cic.term * Utils.comparison) * Cic.metasenv -> 
+    equality
     
 val open_equality :
   equality ->