Goal: remove most of the API (make [Goal.goal] concrete).

We are left with the compatibility layer and a handful of primitives which require some thought to move.

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 *)