From 942fbd2fc1f8ceed520aee164f017cb0ea50bef6 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Thu, 8 Mar 2001 09:07:38 +0000
Subject: changement comparaison etats

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1436 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/eauto.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 9ab7ec5d64..931a7a5559 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -231,8 +231,10 @@ module SearchProblem = struct
   let rec list_addn n x l = 
     if n = 0 then l else x :: (list_addn (pred n) x l)
 
+  (* Ordering of states is lexicographic on depth (greatest first) then
+     number of remaining goals. *)
   let compare s s' =
-    let d = s.depth - s'.depth in
+    let d = s'.depth - s.depth in
     let nbgoals s = List.length (sig_it (fst s.tacres)) in
     if d <> 0 then d else nbgoals s - nbgoals s'
 
-- 
cgit v1.2.3