diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-08 01:42:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-08 02:07:26 +0200 |
| commit | 9d1230d484a2cf519f9cd76dc0f37815f3c6339b (patch) | |
| tree | cde7182712f03ea19b8151584599151818d53c0e /tactics | |
| parent | 2ba1351849550c50e0fe2c7fc7f63758c10fb14a (diff) | |
Fix a heuristic used by legacy typeclass resolution.
The evarmap used by the heuristic could contain resolved evars, which could
lead to a failure of backtracking in the EConstr branch. This is experimental
and may be to costly.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 7eadde78d..ea1966093 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -787,10 +787,10 @@ module V85 = struct let fk' = (fun e -> let do_backtrack = - if unique then occur_existential s' concl + if unique then occur_existential tacgl.sigma concl else if info.unique then true else if List.is_empty gls' then - needs_backtrack env s' info.is_evar concl + needs_backtrack env tacgl.sigma info.is_evar concl else true in let e' = match foundone with None -> e |