diff options
| -rw-r--r-- | proofs/refiner.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 495a9ca826..6a40e2c9d7 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -667,7 +667,9 @@ 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)) pfterm +(* local_strong (whd_betaiotaevar pts.tpf.goal.evar_env (ts_it pts.tpfsigma))*) + local_strong (whd_ise (ts_it pts.tpfsigma)) + pfterm (* Focus on the first leaf proof in a proof-tree state *) |