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 /interp | |
| 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 'interp')
| -rw-r--r-- | interp/constrextern.ml | 5 |
1 files changed, 4 insertions, 1 deletions
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 |