From f46a5686853353f8de733ae7fbd21a3a61977bc7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 3 Feb 2016 15:32:58 +0100
Subject: 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.
---
 proofs/goal.ml      | 5 ++++-
 proofs/proofview.ml | 5 ++++-
 2 files changed, 8 insertions(+), 2 deletions(-)

(limited to 'proofs')

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
-- 
cgit v1.2.3