added a subtle List.rev that makes the order of the equalities taken from the library...

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 1d5d9783fb3bdf4a7df250f67f5b3691e6990183..8e53df28f23e62f9352e2d299633c67f4dd5fedd 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/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 =