diff options
Diffstat (limited to 'proofs/refiner.ml')
| -rw-r--r-- | proofs/refiner.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index fca4d85fe..37a41cd25 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -664,10 +664,11 @@ let extract_pftreestate pts = if subgoals <> [] then errorlabstrm "extract_proof" [< 'sTR "Attempt to save an incomplete proof" >]; -(* local_strong (whd_betaiotaevar pts.tpf.goal.evar_env (ts_it pts.tpfsigma))*) - local_strong (whd_ise (ts_it pts.tpfsigma)) - pfterm - + (*** + let env = Global.env_of_context pts.tpf.goal.evar_hyps in + strong whd_betaiotaevar env (ts_it pts.tpfsigma) pfterm + ***) + local_strong (whd_ise (ts_it pts.tpfsigma)) pfterm (* Focus on the first leaf proof in a proof-tree state *) |