X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Findex.ml;h=beb3aed86da325f6369d99338237f53e0b9a0567;hb=8e4367191fdfd125596658e35d4b99cd3047a5bc;hp=633c32854b284bc79c246515865872dbf01f91e7;hpb=39a2078b0e835d39895a5b6c0862d668ece544f3;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml
index 633c32854..beb3aed86 100644
--- 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) ->