]> matita.cs.unibo.it Git - helm.git/commitdiff
fixed demodulation_goal (used to return always false)
authorAndrea Asperti <andrea.asperti@unibo.it>
Wed, 26 Apr 2006 13:23:55 +0000 (13:23 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Wed, 26 Apr 2006 13:23:55 +0000 (13:23 +0000)
helm/software/components/tactics/paramodulation/indexing.ml

index d71e7c5a793702bbdd2210f40b9f44ebe5146699..1f9f5d5762e3c5b4072e343a5d0458ad7a238d7b 100644 (file)
@@ -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
 ;;