From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 29 Sep 2006 17:07:06 +0000 (+0000)
Subject: removed bad guard that was always false (assert false in the line above)
X-Git-Tag: make_still_working~6827
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=inline;h=bd4a73c6f758bd39254178dd7b313af321a5cd4b;p=helm.git

removed bad guard that was always false (assert false in the line above)
---

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index 546fff631..ff5bf23cb 100644
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -601,8 +601,8 @@ let rec demodulation_equality bag ?from eq_uri newmeta env table target =
     | 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
+          if (Equality.is_weak_identity newtarget) (* || *)
+            (*Equality.meta_convertibility_eq target newtarget*) then
               newmeta, newtarget
           else 
             demodulation_equality bag ?from eq_uri newmeta env table newtarget
@@ -843,7 +843,7 @@ let superposition_right bag
   in
   let new1 = List.map (build_new U.Gt) res1
   and new2 = List.map (build_new U.Lt) res2 in
-  let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
+  let ok e = not (Equality.is_weak_identity (*metasenv', context, ugraph*) e) in
   (!maxmeta,
    (List.filter ok (new1 @ new2)))
 ;;