X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fterms.ml;h=0118df7c18ea4f3fc2cdcd17aaad1a2f2daeaa82;hb=c091ca7a030a85a529543de98e45c54284028b63;hp=bcc3bcf7bd8a05ff4906f35abafcd6491de67eb2;hpb=96c91e470f670018df67c9cbff62fa06e3b57c5e;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/terms.ml b/helm/software/components/ng_paramodulation/terms.ml
index bcc3bcf7b..0118df7c1 100644
--- a/helm/software/components/ng_paramodulation/terms.ml
+++ b/helm/software/components/ng_paramodulation/terms.ml
@@ -67,5 +67,6 @@ module type Blob =
     val pp : t -> string
     val embed : t -> t foterm
     val saturate : t -> t -> t foterm * t foterm
+    val mk_proof : t bag -> int -> int list -> t
   end