attempt to run a last chance procedure after the timeout

[helm.git] / helm / software / components / ng_paramodulation / superposition.mli

diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli
index a7badaba4a5bb32769af0cc4f7bad2322fda7f4b..52011c3e806893d3ca2a8854ce135454ea8586a3 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.mli
+++ b/helm/software/components/ng_paramodulation/superposition.mli
@@ -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 ->