X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fterms.ml;h=1d1465f9e6d7cfe5525792835ddafed373f44706;hb=65e1aa022da79a3a880f5c2d5d0d512b80e50635;hp=46f83544fef9aaba0cdcc19210bb91df96657895;hpb=8de1a75899a83dd31e856804bd448c1bd87d9ab3;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/terms.ml b/helm/software/components/ng_paramodulation/terms.ml
index 46f83544f..1d1465f9e 100644
--- a/helm/software/components/ng_paramodulation/terms.ml
+++ b/helm/software/components/ng_paramodulation/terms.ml
@@ -56,7 +56,7 @@ module OT =
 module M : Map.S with type key = int 
   = Map.Make(OT) 
 
-type 'a bag = 'a unit_clause M.t
+type 'a bag = ('a unit_clause * bool) M.t
 
 module type Blob =
   sig
@@ -65,8 +65,8 @@ module type Blob =
     val compare : t -> t -> int
     val eqP : t
     val pp : t -> string
-    val embed : t -> t foterm
-    val saturate : t -> t -> t foterm * t foterm
-    val mk_proof : t bag -> int list -> t
+    type input
+    val embed : input -> t foterm
+    val saturate : input -> input -> t foterm * t foterm
   end