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.
---
 stm/stm.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 705d427f4b..74a998a74f 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1097,9 +1097,9 @@ module SubTask = struct
       let t, uc = Future.purify (fun () ->
         vernac_interp r_state_fb r_ast;
         let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in
-        match Goal.solution sigma r_goal with
-        | None -> Errors.errorlabstrm "Stm" (str "no progress")
-        | Some t ->
+        match Evd.(evar_body (find sigma r_goal)) with
+        | Evd.Evar_empty -> Errors.errorlabstrm "Stm" (str "no progress")
+        | Evd.Evar_defined t ->
             let t = Evarutil.nf_evar sigma t in
             if Evarutil.is_ground_term sigma t then
               t, Evd.evar_universe_context sigma
-- 
cgit v1.2.3