X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.mli;h=d890a719d6a8a403c693e86591b401aebc02e980;hb=4693f3b9de6d867921b51f61e9a7dc36c3da1b77;hp=0c9a75e62478dff464ea8ee5b5451b662939a1a4;hpb=61f3a8a688132be943b81befa5805e27148f2038;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/saturation.mli b/helm/software/components/tactics/paramodulation/saturation.mli
index 0c9a75e62..d890a719d 100644
--- a/helm/software/components/tactics/paramodulation/saturation.mli
+++ b/helm/software/components/tactics/paramodulation/saturation.mli
@@ -33,35 +33,38 @@ val reset_refs : unit -> unit
 val make_active: Equality.equality list -> active_table
 val make_passive: Equality.equality list -> passive_table
 val add_to_passive: Equality.equality list -> passive_table -> passive_table
+val add_to_active: 
+      Equality.equality_bag -> 
+      active_table -> passive_table ->
+      Utils.environment -> Cic.term (* ty *) -> Cic.term -> Cic.metasenv ->
+          active_table * passive_table * Equality.equality_bag 
 val list_of_passive: passive_table -> Equality.equality list
+val list_of_active: active_table -> Equality.equality list
 
 val simplify_equalities : 
   Equality.equality_bag ->
   UriManager.uri ->
   Utils.environment -> 
   Equality.equality list -> 
-  Equality.equality list
+  Equality.equality_bag * Equality.equality list
 val pump_actives :
   Cic.context ->
   Equality.equality_bag ->
-  int ->
   active_table ->
   passive_table -> 
   int -> 
   float -> 
-  active_table * passive_table * int
+  active_table * passive_table * Equality.equality_bag
 val all_subsumed :
   Equality.equality_bag ->
-  int ->
   ProofEngineTypes.status ->
   active_table ->
   passive_table -> 
   (Cic.substitution * 
      ProofEngineTypes.proof * 
-     ProofEngineTypes.goal list) list * int
+     ProofEngineTypes.goal list) list
 val given_clause: 
   Equality.equality_bag ->
-  int -> (* maxmeta *)
   ProofEngineTypes.status ->
   active_table ->
   passive_table -> 
@@ -69,6 +72,15 @@ val given_clause:
     (Cic.substitution * 
      ProofEngineTypes.proof * 
      ProofEngineTypes.goal list) option * 
-    active_table * passive_table * int
-
+    active_table * passive_table * Equality.equality_bag
 
+val solve_narrowing: 
+  Equality.equality_bag ->
+  ProofEngineTypes.status ->
+  active_table ->
+  passive_table -> 
+  int -> 
+    (Cic.substitution * 
+     ProofEngineTypes.proof * 
+     ProofEngineTypes.goal list) option * 
+    active_table * passive_table * Equality.equality_bag