Various architectural changes

[helm.git] / helm / software / components / ng_paramodulation / terms.mli

diff --git a/helm/software/components/ng_paramodulation/terms.mli b/helm/software/components/ng_paramodulation/terms.mli
index 90ccaf5915b86d2ea7b6152ea6f766adf54f6def..c15c85af24a6c4a91d756441a738d4be2833be27 100644 (file)
--- 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