From f7a57b8b92611ee8c778adf35efec184b8ea9cf4 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 26 Apr 2006 13:23:55 +0000
Subject: [PATCH] fixed demodulation_goal (used to return always false)

---
 .../software/components/tactics/paramodulation/indexing.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index d71e7c5a7..1f9f5d576 100644
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/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
 ;;
-- 
2.39.2