superposition_left not performed if the input goal is an identity

[helm.git] / helm / software / components / tactics / paramodulation / saturation.mli

diff --git a/helm/software/components/tactics/paramodulation/saturation.mli b/helm/software/components/tactics/paramodulation/saturation.mli
index 9f1ad293d97cfa1563df07112ed52a4bf6b3b642..8a03cd547a0be220daae305c3f44c379ca9b9524 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.mli
+++ b/helm/software/components/tactics/paramodulation/saturation.mli
@@ -27,6 +27,7 @@
 
 
 val saturate :
+  bool ->
   HMysql.dbd ->
   ?full:bool ->
   ?depth:int ->