X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.mli;h=30d32d540a330d8bdb9495b086a134e0fffd5391;hb=72cd94b68037956a70b98cfa54f316fd54e52bae;hp=e3e2f8b9f2f6f15d12c791a4351309f022139ccd;hpb=2c2b31c242aa81dc6f3c73e7e2a3ec0789a21edd;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli
index e3e2f8b9f..30d32d540 100644
--- a/helm/software/components/ng_paramodulation/superposition.mli
+++ b/helm/software/components/ng_paramodulation/superposition.mli
@@ -11,7 +11,7 @@
 
 (* $Id: index.mli 9822 2009-06-03 15:37:06Z tassi $ *)
 
-module Superposition (B : Terms.Blob) : 
+module Superposition (B : Orderings.Blob) : 
   sig
 
                         (* bag, maxvar, meeting point *)
@@ -45,7 +45,8 @@ module Superposition (B : Terms.Blob) :
             B.t Terms.bag * (B.t Terms.unit_clause option)
 
     (* may raise success *)
-    val simplify_goal : 
+    val simplify_goal :
+          no_demod:bool ->
           int ->
           Index.Index(B).DT.t ->
           B.t Terms.bag ->
@@ -58,7 +59,7 @@ module Superposition (B : Terms.Blob) :
       Index.Index(B).active_set ->
       B.t Terms.bag ->
       int ->
-      (B.t Terms.unit_clause * B.t Terms.bag * Index.Index(B).active_set) option
+      B.t Terms.bag * (B.t Terms.unit_clause * Index.Index(B).active_set) option
 
 
     val keep_simplified:
@@ -66,7 +67,13 @@ module Superposition (B : Terms.Blob) :
       Index.Index(B).active_set ->
       B.t Terms.bag ->
       int ->
-      (B.t Terms.unit_clause * B.t Terms.bag * Index.Index(B).active_set) option
+      B.t Terms.bag * (B.t Terms.unit_clause * Index.Index(B).active_set) option
+
+    val  orphan_murder:
+      B.t Terms.bag ->
+      B.t Terms.unit_clause list ->
+      B.t Terms.unit_clause ->
+      bool
 
 
   end