From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 6 Nov 2008 09:39:29 +0000 (+0000)
Subject: the passive set and passive list are expected to have the same cardinality, that... 
X-Git-Tag: make_still_working~4594
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0e3324ad8e6a552ee89f02371412f7bc2e83379f;hp=05b38c588708726f48288227221a8b706544b0a7;p=helm.git

the passive set and passive list are expected to have the same cardinality, that was was some bad reason not always the case
---

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 7cb9fb0e5..5fa1dafeb 100644
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -125,8 +125,11 @@ let make_passive eq_list =
   let set =
     List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty eq_list
   in
-  (*EqualitySet.elements set*) eq_list, set (* see applys.ma *)
+  (* we have the invariant that the list and the set have the same
+   * cardinality *)
+  EqualitySet.elements set, set
 ;;
+
 let make_empty_active () = [], Indexing.empty ;;
 let make_active eq_list = 
   eq_list, List.fold_left Indexing.index Indexing.empty eq_list
@@ -134,6 +137,7 @@ let make_active eq_list =
 
 let size_of_passive (passive_list, _) = List.length passive_list;;
 let size_of_active (active_list, _) = List.length active_list;;
+
 let passive_is_empty = function
   | [], s when EqualitySet.is_empty s -> true
   | [], s -> assert false (* the set and the list should be in sync *)