diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-03 15:32:58 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-13 17:26:35 +0100 |
| commit | f46a5686853353f8de733ae7fbd21a3a61977bc7 (patch) | |
| tree | 0d26cb4280faa70491d83d7665466c9c1ad6d2d5 /proofs/proofview.ml | |
| parent | df6bb883920e3a03044d09f10b57a44a2e7c5196 (diff) | |
Do not give a name to anonymous evars anymore. See bug #4547.
The current solution may not be totally ideal though. We generate names for
anonymous evars on the fly at printing time, based on the Evar_kind data they
are wearing. This means in particular that the printed name of an anonymous
evar may change in the future because some unrelate evar has been solved or
introduced.
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 |