First tests for paramodulation (pretty printer, unification)

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

diff --git a/helm/software/components/ng_paramodulation/terms.ml b/helm/software/components/ng_paramodulation/terms.ml
index 72e32987a00efd3b39f30f27920b7f696b33ea2a..38e1723c20c3368bacc3861565335620733fa6b5 100644 (file)
--- a/helm/software/components/ng_paramodulation/terms.ml
+++ b/helm/software/components/ng_paramodulation/terms.ml
@@ -64,6 +64,7 @@ module type Blob =
     val eq : t -> t -> bool
     val compare : t -> t -> int
     val pp : t -> string
+    val embed : t -> t foterm * int list
   end
 
 module Utils (B : Blob) = struct