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

1 files changed, 8 insertions, 15 deletions

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)