From 549c0abf3f9d170db297a8b9d35bf4bf97288662 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 2 Oct 2006 15:33:24 +0000 Subject: [PATCH] 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 --- components/tactics/paramodulation/saturation.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 = -- 2.39.2