almost complete superposition right step

[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 6c26e7b86ab82cfeab8996b743d076bd614560f3..3c203d3a7131e7ce1d2411f950975a29c19d9753 100644 (file)
--- a/helm/software/components/ng_paramodulation/index.ml
+++ b/helm/software/components/ng_paramodulation/index.ml
@@ -93,4 +93,6 @@ module Index(B : Terms.Blob) = struct
           DT.index t p (Terms.Nodir, c)
   ;;
 
+  type active_set = B.t Terms.unit_clause list * DT.t
+
 end