From 9cf6b3543bf369ccb4d3b0909ee3db96e074e24e Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 10 Feb 2010 00:14:07 +0000
Subject: Fix [Existing Class] impl and add documentation. Fix computation of
 the dependency order of obligations that was not backwards-compatible.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12719 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/subtac/eterm.ml | 23 ++++++++---------------
 1 file changed, 8 insertions(+), 15 deletions(-)

(limited to 'plugins')

diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml
index d9b73109a2..4b95df197d 100644
--- a/plugins/subtac/eterm.ml
+++ b/plugins/subtac/eterm.ml
@@ -143,21 +143,14 @@ let evar_dependencies evm ev =
   in aux (Intset.singleton ev)
 
 let sort_dependencies evl =
-  let one_step deps ine oute =
-    List.fold_left (fun (ine, oute, acc) (id, _, deps' as d) -> 
-      if not (Intset.mem id deps) then
-	if Intset.subset deps' (Intset.add id deps) then
-	  (d :: ine, oute, Intset.add id acc)
-	else (ine, d :: oute, acc)
-      else (ine, oute, acc))
-      (ine, [], deps) oute
-  in
-  let rec aux deps evsin evsout =
-    let (evsin, evsout, deps') = one_step deps evsin evsout in
-      if evsout = [] then List.rev evsin
-      else aux deps' evsin evsout
-  in aux Intset.empty [] evl
-
+  List.stable_sort
+    (fun (id, ev, deps) (id', ev', deps') ->
+      if id = id' then 0
+      else if Intset.mem id deps' then -1
+      else if Intset.mem id' deps then 1
+      else Pervasives.compare id id')
+    evl
+      
 let map_evar_body f = function
   | Evar_empty -> Evar_empty
   | Evar_defined c -> Evar_defined (f c)
-- 
cgit v1.2.3