X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fterms.mli;fp=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fterms.mli;h=c15c85af24a6c4a91d756441a738d4be2833be27;hb=38c54dd8e2234836d5f3e8011c478daf7d59fa25;hp=90ccaf5915b86d2ea7b6152ea6f766adf54f6def;hpb=8a3045a162622e8a76ffdb267309faff496ee7ec;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/terms.mli b/helm/software/components/ng_paramodulation/terms.mli
index 90ccaf591..c15c85af2 100644
--- a/helm/software/components/ng_paramodulation/terms.mli
+++ b/helm/software/components/ng_paramodulation/terms.mli
@@ -97,10 +97,5 @@ module type Blob =
      * *)
     val pp : t -> string
 
-    type input
-    val embed : input -> t foterm
-    (* saturate [proof] [type] -> [proof] * [type] *)
-    val saturate : input -> input -> t foterm * t foterm
-
   end