X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.mli;h=d890a719d6a8a403c693e86591b401aebc02e980;hb=25564c06c570e5ab9be455904c0b381842f8d4c4;hp=71764cddd2ce619c35a1b291248f6b5cc1f7c267;hpb=91f0c0e84bfe6bf22e960d466e16f7260a2882ee;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/saturation.mli b/helm/software/components/tactics/paramodulation/saturation.mli
index 71764cddd..d890a719d 100644
--- a/helm/software/components/tactics/paramodulation/saturation.mli
+++ b/helm/software/components/tactics/paramodulation/saturation.mli
@@ -74,3 +74,13 @@ val given_clause:
      ProofEngineTypes.goal list) option * 
     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