From 07d169f337cdb5dffcf2d508c1bac791a60b38d7 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 --- helm/software/components/tactics/paramodulation/saturation.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index 1d5d9783f..8e53df28f 100644 --- 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 = -- 2.39.2