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.
---
 interp/constrextern.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 9df8f9c233..cc5d189e04 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -988,7 +988,10 @@ let rec glob_of_pat env sigma = function
   | PEvar (evk,l) ->
       let test (id,_,_) = function PVar id' -> Id.equal id id' | _ -> false in
       let l = Evd.evar_instance_array test (Evd.find sigma evk) l in
-      let id = Evd.evar_ident evk sigma in
+      let id = match Evd.evar_ident evk sigma with
+      | None -> Id.of_string "__"
+      | Some id -> id
+      in
       GEvar (loc,id,List.map (on_snd (glob_of_pat env sigma)) l)
   | PRel n ->
       let id = try match lookup_name_of_rel n env with
-- 
cgit v1.2.3