Build_proof_goal does not return the metasenv any more.

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

diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index d71e7c5a793702bbdd2210f40b9f44ebe5146699..f3314bfa022d461b81c63de3f9921db6d6a8fa04 100644 (file)
--- a/components/tactics/paramodulation/indexing.ml
+++ b/components/tactics/paramodulation/indexing.ml
@@ -602,7 +602,7 @@ let rec demodulation_equality ?from newmeta env table sign target =
   let order = !Utils.compare_terms left right in
   let stat = (eq_ty, left, right, order) in 
   let w = Utils.compute_equality_weight stat in
-  let target = Equality.mk_equality (w, proof, stat, metas) in
+  (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
   if Utils.debug_metas then 
     ignore(check_target context target "demod equalities input");
   let metasenv' = (* metasenv @ *) metas in
@@ -745,6 +745,7 @@ let rec demodulation_equality ?from newmeta env table sign target =
     match res with
     | Some t ->
         let newmeta, newtarget = build_newtarget true t in
+         assert (not (Equality.meta_convertibility_eq target newtarget));
           if (Equality.is_weak_identity newtarget) ||
             (Equality.meta_convertibility_eq target newtarget) then
               newmeta, newtarget
@@ -1202,9 +1203,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
 ;;