Fixes

[helm.git] / helm / software / components / ng_paramodulation / index.ml

diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml
index 633c32854b284bc79c246515865872dbf01f91e7..beb3aed86da325f6369d99338237f53e0b9a0567 100644 (file)
--- a/helm/software/components/ng_paramodulation/index.ml
+++ b/helm/software/components/ng_paramodulation/index.ml
@@ -86,6 +86,7 @@ module Index(B : Orderings.Blob) = struct
     = Make(FotermIndexable)(ClauseSet)
 
   let index_literal t c is_pos pos = function
+    | Terms.Equation (l,_,_,Terms.Invertible)
     | Terms.Equation (l,_,_,Terms.Gt) -> 
           DT.index t l (Terms.Left2Right,is_pos,pos,c)
     | Terms.Equation (_,r,_,Terms.Lt) ->