Fixed nasty bug in maxvar updating

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

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 554028fa75b857c3c10ccadf73d6d5cf825404a7..aef672c144f5b2ba307626217ce5d122260a8812 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -451,7 +451,7 @@ module Superposition (B : Terms.Blob) =
         superposition_with_table bag maxvar goal atable 
       in
        debug "Superposed goal with active clauses";
-       (* We demodulate the goal with active clauses *)
+       (* We demodulate the new goals with active clauses *)
       let bag, new_goals = 
         List.fold_left
          (fun (bag, acc) g ->