From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 2 Oct 2006 15:33:24 +0000 (+0000)
Subject: added a subtle List.rev that makes the order of the equalities taken from the library... 
X-Git-Tag: 0.4.95@7852~952
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=549c0abf3f9d170db297a8b9d35bf4bf97288662;p=helm.git

added a subtle List.rev that makes the order of the equalities taken from the library as it used to be. In this way the applys test works, but is not clear why the other order does not produce a solution in decent time
---

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index 1d5d9783f..8e53df28f 100644
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -120,7 +120,7 @@ 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
+  (*EqualitySet.elements set*) List.rev eq_list, set (* see applys.ma *)
 ;;
 let make_empty_active () = [], Indexing.empty ;;
 let make_active eq_list =