diff options
Diffstat (limited to 'toplevel/whelp.ml4')
| -rw-r--r-- | toplevel/whelp.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index 8929fb32c..8185e5702 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -192,8 +192,8 @@ let whelp_elim ind = send_whelp "elim" (make_string uri_of_global (IndRef ind)) let on_goal f = - let { Evd.it=goals ; sigma=sigma } = Proof.V82.subgoals (get_pftreestate ()) in - let gls = { Evd.it=List.hd goals ; sigma = sigma } in + let gls = Proof.V82.subgoals (get_pftreestate ()) in + let gls = { gls with Evd.it = List.hd gls.Evd.it } in f (Termops.it_mkNamedProd_or_LetIn (pf_concl gls) (pf_hyps gls)) type whelp_request = |