X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Fequality.ml;h=7123c134a93a98056655f6cee83e55600b559945;hb=c049b167b6a59e7a1e755c0f5a4bc00ce0826c48;hp=65593985108f1e42d177074fb2c70957fe9cf6f1;hpb=59895ae358dff2a57a9fd1ea6924690a0862e036;p=helm.git

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index 655939851..7123c134a 100644
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -1003,7 +1003,9 @@ let is_weak_identity eq =
 let is_identity (_, context, ugraph) eq = 
   let _,_,(ty,left,right,_),menv,_ = open_equality eq in
   (* doing metaconv here is meaningless *)
-  fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph)
+  left = right
+(*   fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph)
+ *   *)
 ;;