more transitivity on proofs

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

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index f3314bfa022d461b81c63de3f9921db6d6a8fa04..584bf5c60950c684eeda9e250d00c2c9487c5994 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -593,15 +593,15 @@ let rec demodulation_equality ?from newmeta env table sign target =
   let module HL = HelmLibraryObjects in
   let module U = Utils in
   let metasenv, context, ugraph = env in
-  let w, ((proof_new, proof_old) as proof), 
+  let w, ((proof_new, proof_old) (*as proof*)), 
      (eq_ty, left, right, order), metas, id = 
     Equality.open_equality target in
   (* first, we simplify *)
-  let right = U.guarded_simpl context right in
-  let left = U.guarded_simpl context left in
-  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 right = U.guarded_simpl context right in *)
+(*   let left = U.guarded_simpl context left in *)
+(*   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 *)
   if Utils.debug_metas then 
     ignore(check_target context target "demod equalities input");