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 1f9f5d5762e3c5b4072e343a5d0458ad7a238d7b..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