{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/541","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/541/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/541/comments","events_url":"https://api.github.com/repos/coq/coq/issues/541/events","html_url":"https://github.com/coq/coq/pull/541","id":219823050,"number":541,"title":"Fixing \"decide equality\" bug #5449","user":{"login":"herbelin","id":460771,"avatar_url":"https://avatars2.githubusercontent.com/u/460771?v=3","gravatar_id":"","url":"https://api.github.com/users/herbelin","html_url":"https://github.com/herbelin","followers_url":"https://api.github.com/users/herbelin/followers","following_url":"https://api.github.com/users/herbelin/following{/other_user}","gists_url":"https://api.github.com/users/herbelin/gists{/gist_id}","starred_url":"https://api.github.com/users/herbelin/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/herbelin/subscriptions","organizations_url":"https://api.github.com/users/herbelin/orgs","repos_url":"https://api.github.com/users/herbelin/repos","events_url":"https://api.github.com/users/herbelin/events{/privacy}","received_events_url":"https://api.github.com/users/herbelin/received_events","type":"User","site_admin":false},"labels":[{"id":485985650,"url":"https://api.github.com/repos/coq/coq/labels/bugfix","name":"bugfix","color":"d93f0b","default":false}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":6,"created_at":"2017-04-06T08:30:49Z","updated_at":"2017-05-02T15:32:23Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/541","html_url":"https://github.com/coq/coq/pull/541","diff_url":"https://github.com/coq/coq/pull/541.diff","patch_url":"https://github.com/coq/coq/pull/541.patch"},"body":"Again, I submit this as a PR in case others have better alternative directions to propose, but if time is missing, I could as well commit it directly as a fix.\r\n\r\nThe code was assuming that the terms `t` and `u` for which `{t=u}+{t<>u}` is proved were distinct. We refine an internal `generalize` of `u` so that it works on the two precise occurrences to abstract, even if other occurrences of `u` occur as subterm of `t` too.\r\n\r\nWe also reuse the global constants found in the statement rather than reconstructing them (this seems better in case the global constants eventually get polymorphic universes, no?)."},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/298671019","html_url":"https://github.com/coq/coq/pull/541#issuecomment-298671019","issue_url":"https://api.github.com/repos/coq/coq/issues/541","id":298671019,"user":{"login":"herbelin","id":460771,"avatar_url":"https://avatars2.githubusercontent.com/u/460771?v=3","gravatar_id":"","url":"https://api.github.com/users/herbelin","html_url":"https://github.com/herbelin","followers_url":"https://api.github.com/users/herbelin/followers","following_url":"https://api.github.com/users/herbelin/following{/other_user}","gists_url":"https://api.github.com/users/herbelin/gists{/gist_id}","starred_url":"https://api.github.com/users/herbelin/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/herbelin/subscriptions","organizations_url":"https://api.github.com/users/herbelin/orgs","repos_url":"https://api.github.com/users/herbelin/repos","events_url":"https://api.github.com/users/herbelin/events{/privacy}","received_events_url":"https://api.github.com/users/herbelin/received_events","type":"User","site_admin":false},"created_at":"2017-05-02T15:32:23Z","updated_at":"2017-05-02T15:32:23Z","body":"@Zimmi48: The problem in searching PRs (or Gitter), is that I have to remember one or several discriminating words of the discussion I'm looking for, and this is not necessarily easy to find.\r\n\r\nAn organized wiki would certainly help. I'd be curious about what GitHub can give."}}
{"actor":{"display_login":"herbelin"}}