diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 1f8a57f07f..e0b7624317 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4204,7 +4204,7 @@ let refine_open_constr c env sigma concl = let handle = ref Evar.Set.empty in let sigma, pf = constr_of_open_constr handle c env sigma concl in let sigma = Evarconv.consider_remaining_unif_problems env sigma in - let subgoals = List.map Goal.build (Evar.Set.elements !handle) in + let subgoals = Evar.Set.elements !handle in (subgoals, pf, sigma) (** Tacticals defined directly in term of Proofview *) |