diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2017-06-14 15:37:14 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2017-06-14 15:37:14 +0200 |
| commit | 6c6c045a42dc591a0c35730e0abff80be0c8b9bb (patch) | |
| tree | c92af37b53de9f771ab62ce44e2d5444c604fa19 /tactics/class_tactics.ml | |
| parent | 5bf9c993d3ef15ecf4c6d5c12f23f9c2fe67dfa7 (diff) | |
[typeclasses eauto] Fix bug #3943: non-termination in topological
sorting for the dependency order option.
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 4bde427b1..cb0f66730 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 |