X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Fequality.mli;h=2d7e48e5cb13dd18ba66d6f0f7543622630b26e3;hb=f820f75a0b94bcc6b6d31c9471c8921ce098427d;hp=ea0cefd55113dca76d0f48b236246a2363fbdc2e;hpb=6421979dbececb04f6ab0d3534f2489d7f151c5f;p=helm.git

diff --git a/components/tactics/paramodulation/equality.mli b/components/tactics/paramodulation/equality.mli
index ea0cefd55..2d7e48e5c 100644
--- a/components/tactics/paramodulation/equality.mli
+++ b/components/tactics/paramodulation/equality.mli
@@ -70,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 ->