initial import of standalone matitaprover binary

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

diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml
index f56cccd89933b5dde4a4da6b434fb5b9c9312a39..26b7f6fa4b2e1abec80070352d5dbb502d1f99b8 100644 (file)
--- a/helm/software/components/ng_paramodulation/foUtils.ml
+++ b/helm/software/components/ng_paramodulation/foUtils.ml
@@ -140,9 +140,13 @@ module Utils (B : Terms.Blob) = struct
     (Order.compute_unit_clause_weight cl, cl)
   ;;
 
-  let compare_passive_clauses (w1,(id1,_,_,_)) (w2,(id2,_,_,_)) =
+  let compare_passive_clauses_weight (w1,(id1,_,_,_)) (w2,(id2,_,_,_)) =
     if w1 = w2 then id1 - id2
     else w1 - w2
   ;;
 
+  let compare_passive_clauses_age (_,(id1,_,_,_)) (_,(id2,_,_,_)) =
+    id1 - id2
+  ;;
+
 end