From 91f34a0a6744a06cb65c9ffe387f54f857a7bb28 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Mon, 13 Oct 2014 14:35:07 +0200
Subject: 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.
---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

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 *)
-- 
cgit v1.2.3