From b618c488ec6b128767af82128d1d4d953cf5c8af Mon Sep 17 00:00:00 2001
From: denes <??>
Date: Fri, 25 Sep 2009 22:27:12 +0000
Subject: [PATCH] Fixed typo
---
.../software/components/ng_paramodulation/superposition.ml | 7 +++----
1 file changed, 3 insertions(+), 4 deletions(-)
diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index c5db7a4e2..bc4f651a4 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -280,8 +280,8 @@ module Superposition (B : Orderings.Blob) =
let rec demod_lit ~jump_to_right bag id lit clause_ctx =
(match lit with
| Terms.Predicate t -> assert false
- | Terms.Equation (l,r,ty,_) -> assert false
- (*let bag,l,id1,lit =
+ | Terms.Equation (l,r,ty,_) ->
+ let bag,l,id1,lit =
visit bag [2]
(fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) id lit l
(ctx_demod table vl clause_ctx)
@@ -291,8 +291,7 @@ module Superposition (B : Orderings.Blob) =
(fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) id1 lit r
(ctx_demod table vl clause_ctx)
in
- let cl,_,_ = Terms.get_from_bag id2 bag in
- bag,id2,cl *) )
+ bag,id2,lit)
in
let nlit,_,bag,id = if nlit = [] then nlit,[],bag,id
else List.fold_left
--
2.39.2