From bd4a73c6f758bd39254178dd7b313af321a5cd4b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 29 Sep 2006 17:07:06 +0000 Subject: [PATCH] removed bad guard that was always false (assert false in the line above) --- helm/software/components/tactics/paramodulation/indexing.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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))) ;; -- 2.39.2