diff options
Diffstat (limited to 'proofs/proofview.ml')
| -rw-r--r-- | proofs/proofview.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index a6d9735f1..49228c93a 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -1093,7 +1093,10 @@ struct | None -> Evd.define gl.Goal.self c sigma | Some evk -> let id = Evd.evar_ident gl.Goal.self sigma in - Evd.rename evk id (Evd.define gl.Goal.self c sigma) + let sigma = Evd.define gl.Goal.self c sigma in + match id with + | None -> sigma + | Some id -> Evd.rename evk id sigma in (** Restore the [future goals] state. *) let sigma = Evd.restore_future_goals sigma prev_future_goals prev_principal_goal in |