diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-19 23:54:21 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-19 23:54:21 +0200 |
| commit | 6cc617b570da186c3a80eb5219715bf244c45627 (patch) | |
| tree | 9e9185febbdaea8aa3e3c34dd9b617f48de4c7b9 /tactics/class_tactics.ml | |
| parent | ff56c76126784897fe0df6f2443fc738245a40a2 (diff) | |
| parent | 6c6c045a42dc591a0c35730e0abff80be0c8b9bb (diff) | |
Merge PR#787: [typeclasses eauto] Fix bug #3943: non-termination in topological
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 5fbf59b81..30063ce37 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 |