diff options
| author | Pierre-Marie Pédrot | 2016-02-03 15:32:58 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-02-13 17:26:35 +0100 |
| commit | f46a5686853353f8de733ae7fbd21a3a61977bc7 (patch) | |
| tree | 0d26cb4280faa70491d83d7665466c9c1ad6d2d5 /proofs | |
| 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')
| -rw-r--r-- | proofs/goal.ml | 5 | ||||
| -rw-r--r-- | proofs/proofview.ml | 5 |
2 files changed, 8 insertions, 2 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index 1dd5be0e71..43a3024e50 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -89,7 +89,10 @@ module V82 = struct (* Instantiates a goal with an open term, using name of goal for evk' *) let partial_solution_to sigma evk evk' c = let id = Evd.evar_ident evk sigma in - Evd.rename evk' id (partial_solution sigma evk c) + let sigma = partial_solution sigma evk c in + match id with + | None -> sigma + | Some id -> Evd.rename evk' id sigma (* Parts of the progress tactical *) let same_goal evars1 gl1 evars2 gl2 = diff --git a/proofs/proofview.ml b/proofs/proofview.ml index a6d9735f14..49228c93ac 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 |