Final subst returned by superposition and passed around.

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

diff --git a/helm/software/components/ng_paramodulation/paramod.mli b/helm/software/components/ng_paramodulation/paramod.mli
index b161ae459086fa5bfe406545521ebcfd4545d82b..321d0f8971730f03a2d7b06ccce9e63d5634956a 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.mli
+++ b/helm/software/components/ng_paramodulation/paramod.mli
@@ -17,7 +17,8 @@ module type Paramod =
     type input
     type state
     type szsontology = 
-      | Unsatisfiable of (t Terms.bag * int * int list) list
+      | Unsatisfiable of 
+         (t Terms.bag * int * t Terms.substitution * int list) list
       | GaveUp 
       | Error of string 
       | Timeout of int * t Terms.bag