fixed demodulation_goal (used to return always false)

[helm.git] / components / tactics / paramodulation / indexing.ml

diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index d71e7c5a793702bbdd2210f40b9f44ebe5146699..1f9f5d5762e3c5b4072e343a5d0458ad7a238d7b 100644 (file)
--- a/components/tactics/paramodulation/indexing.ml
+++ b/components/tactics/paramodulation/indexing.ml
@@ -1202,9 +1202,12 @@ let rec demodulation_goal newmeta env table goal =
       let newmeta, newgoal = build_newgoal t in
       let _, _, newg = newgoal in
       if Equality.meta_convertibility term newg then
-        true, newmeta, newgoal
+        false, newmeta, newgoal
       else
-        demodulation_goal newmeta env table newgoal
+        let changed, newmeta, newgoal = 
+         demodulation_goal newmeta env table newgoal 
+       in
+       true, newmeta, newgoal
   | None ->
       false, newmeta, goal
 ;;