diff options
| author | Matthieu Sozeau | 2014-09-15 12:12:41 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-15 12:16:52 +0200 |
| commit | e2c0cd1cb7fd06ef37f87f64e1164766820c16ea (patch) | |
| tree | 304136bb445837742e6b4208ec0bfaf41a062bab /tactics/class_tactics.ml | |
| parent | 92682297f528c3570dc8449118d2f2cd2be7cc53 (diff) | |
Avoid backtracking in typeclass search if a solution for a closed
non-dependent or propositional constraint has already been found
(same behavior as before previous patch).
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 29cc6f51ac..77101c70e6 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -442,7 +442,14 @@ let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk | _ -> second.skft (fun {it=gls';sigma=s'} fk' -> - aux s' (gls'::acc) fk' gls) + let fk'' = + if not info.unique && List.is_empty gls' && + not (needs_backtrack (Goal.V82.env s gl) s + info.is_evar (Goal.V82.concl s gl)) + then fk + else fk' + in + aux s' (gls'::acc) fk'' gls) fk {it = (gl,info); sigma = s; }) | [] -> Somek2 (List.rev acc, s, fk) in fun {it = gls; sigma = s; } fk -> |