From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 26 Apr 2006 13:23:55 +0000 (+0000)
Subject: fixed demodulation_goal (used to return always false)
X-Git-Tag: 0.4.95@7852~1493
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c6d4fef535f3e4c5e8b8d3c83820e823bb69bbc9;p=helm.git

fixed demodulation_goal (used to return always false)
---

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