diff options
author | Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-13 14:35:07 +0200 |
---|---|---|
committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-16 10:37:27 +0200 |
commit | 91f34a0a6744a06cb65c9ffe387f54f857a7bb28 (patch) | |
tree | efb79f216193a2f0e73683a03c32d36f1461f2c4 /stm | |
parent | 2e4b5351c9bcca1ccba37075fe3873562969fd3e (diff) |
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.
Diffstat (limited to 'stm')
-rw-r--r-- | stm/stm.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 705d427f4..74a998a74 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 |