{"action":"closed","issue":{"url":"https://api.github.com/repos/leanprover/lean/issues/755","labels_url":"https://api.github.com/repos/leanprover/lean/issues/755/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/lean/issues/755/comments","events_url":"https://api.github.com/repos/leanprover/lean/issues/755/events","html_url":"https://github.com/leanprover/lean/issues/755","id":97963478,"number":755,"title":"metavariables in displayed goal","user":{"login":"fpvandoorn","id":7376012,"avatar_url":"https://avatars.githubusercontent.com/u/7376012?v=3","gravatar_id":"","url":"https://api.github.com/users/fpvandoorn","html_url":"https://github.com/fpvandoorn","followers_url":"https://api.github.com/users/fpvandoorn/followers","following_url":"https://api.github.com/users/fpvandoorn/following{/other_user}","gists_url":"https://api.github.com/users/fpvandoorn/gists{/gist_id}","starred_url":"https://api.github.com/users/fpvandoorn/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/fpvandoorn/subscriptions","organizations_url":"https://api.github.com/users/fpvandoorn/orgs","repos_url":"https://api.github.com/users/fpvandoorn/repos","events_url":"https://api.github.com/users/fpvandoorn/events{/privacy}","received_events_url":"https://api.github.com/users/fpvandoorn/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":3,"created_at":"2015-07-29T15:33:31Z","updated_at":"2015-07-29T23:42:47Z","closed_at":"2015-07-29T23:42:47Z","body":"In [this gist](https://gist.github.com/fpvandoorn/75f20b0fee0682a7f8e6), when hovering over the comma after `exact f (tr a)` on line 57 and then pressing `C-c C-g` I get\r\n```lean\r\nposition 57:52\r\nA : Type,\r\nB : Type,\r\nf : one_step_tr A → B\r\n⊢ Π (x y : A),\r\n    ?M_1 = ?M_1\r\n```\r\nHowever, `*lean-info*` shows the goal without metavariables (as expected):\r\n```lean\r\nA : Type,\r\nB : Type,\r\nf : one_step_tr A → B\r\n⊢ Π (x y : A),\r\n    f (tr x) = f (tr y)\r\n```"}}