From c6d4fef535f3e4c5e8b8d3c83820e823bb69bbc9 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 26 Apr 2006 13:23:55 +0000 Subject: [PATCH] fixed demodulation_goal (used to return always false) --- components/tactics/paramodulation/indexing.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) 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 ;; -- 2.39.2