coercions are there, but not heavily tested

[helm.git] / helm / software / components / tactics / paramodulation / saturation.ml

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index c8ab4e428cfecdc9f9e92f672b55fdb532b00f52..5fa1dafeb288c537e1d67a98d2b7ebd6ec6880b1 100644 (file)
--- 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 *)
@@ -1623,7 +1627,12 @@ let all_subsumed bag maxm status active passive =
                status goalproof newproof subsumption_id subsumption_subst proof_menv
           in
           let uri, metasenv, subst, meta_proof, term_to_prove, attrs = proof in
-          let proof = uri, other_menv@metasenv, subst, meta_proof, term_to_prove, attrs in
+           let newmetasenv = 
+             other_menv @ 
+             List.filter
+               (fun x,_,_ -> not (List.exists (fun y,_,_ -> x=y) other_menv)) metasenv
+           in
+          let proof = uri, newmetasenv, subst, meta_proof, term_to_prove, attrs in
             (subst, proof,gl)) subsumed_or_id 
   in 
   res, !maxmeta