Active goals are now demodulated after selecting a positive clause.

[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 5878918c2b37d60c1a8b8a4b63758d927882b229..cce81944bd497d286b50c22c31d4055c3c4e5228 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.mli
+++ b/helm/software/components/ng_paramodulation/superposition.mli
@@ -14,6 +14,7 @@
 module Superposition (B : Terms.Blob) : 
   sig
 
+                        (* bag, maxvar, meeting point *)
     exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
 
     (* The returned active set is the input one + the selected clause *)