From 6c6c045a42dc591a0c35730e0abff80be0c8b9bb Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 14 Jun 2017 15:37:14 +0200
Subject: [typeclasses eauto] Fix bug #3943: non-termination in topological

sorting for the dependency order option.
---
 tactics/class_tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 4bde427b15..cb0f66730a 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -527,10 +527,10 @@ let top_sort evm undefs =
   let tosee = ref undefs in
   let rec visit ev evi =
     let evs = Evarutil.undefined_evars_of_evar_info evm evi in
+      tosee := Evar.Map.remove ev !tosee;
       Evar.Set.iter (fun ev ->
         if Evar.Map.mem ev !tosee then
           visit ev (Evar.Map.find ev !tosee)) evs;
-      tosee := Evar.Map.remove ev !tosee;
       l' := ev :: !l';
   in
     while not (Evar.Map.is_empty !tosee) do
-- 
cgit v1.2.3