Minor changes.

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

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index 65593985108f1e42d177074fb2c70957fe9cf6f1..7123c134a93a98056655f6cee83e55600b559945 100644 (file)
--- 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)
+ *   *)
 ;;