diff options
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e4503dab6..a6bc805bd 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1672,6 +1672,7 @@ let solve_remaining_apply_goals = let env = Proofview.Goal.env gl in let evd = Sigma.to_evar_map sigma in let concl = Proofview.Goal.concl gl in + let concl = EConstr.of_constr concl in if Typeclasses.is_class_type evd concl then let evd', c' = Typeclasses.resolve_one_typeclass env evd concl in let tac = Refine.refine ~unsafe:true { run = fun h -> Sigma.here c' h } in |