{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/402","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/402/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/402/comments","events_url":"https://api.github.com/repos/coq/coq/issues/402/events","html_url":"https://github.com/coq/coq/pull/402","id":200902162,"number":402,"title":"Uniform attribute handling in interfaces","user":{"login":"ejgallego","id":7192257,"avatar_url":"https://avatars1.githubusercontent.com/u/7192257?v=3","gravatar_id":"","url":"https://api.github.com/users/ejgallego","html_url":"https://github.com/ejgallego","followers_url":"https://api.github.com/users/ejgallego/followers","following_url":"https://api.github.com/users/ejgallego/following{/other_user}","gists_url":"https://api.github.com/users/ejgallego/gists{/gist_id}","starred_url":"https://api.github.com/users/ejgallego/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ejgallego/subscriptions","organizations_url":"https://api.github.com/users/ejgallego/orgs","repos_url":"https://api.github.com/users/ejgallego/repos","events_url":"https://api.github.com/users/ejgallego/events{/privacy}","received_events_url":"https://api.github.com/users/ejgallego/received_events","type":"User","site_admin":false},"labels":[{"id":485985791,"url":"https://api.github.com/repos/coq/coq/labels/cleanup","name":"cleanup","color":"0052cc","default":false},{"id":485986179,"url":"https://api.github.com/repos/coq/coq/labels/feature","name":"feature","color":"0e8a16","default":false},{"id":396673733,"url":"https://api.github.com/repos/coq/coq/labels/redesign","name":"redesign","color":"fef2c0","default":false},{"id":394846579,"url":"https://api.github.com/repos/coq/coq/labels/Request%208.7%20inclusion","name":"Request 8.7 inclusion","color":"bfdadc","default":false}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":47,"created_at":"2017-01-15T22:27:14Z","updated_at":"2017-04-25T21:31:46Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/402","html_url":"https://github.com/coq/coq/pull/402","diff_url":"https://github.com/coq/coq/pull/402.diff","patch_url":"https://github.com/coq/coq/pull/402.patch"},"body":"This patch switches all Coq interfaces, (in particular the ones in `intf`) to use `Loc.located` and `CAst.ast`. The idea is to uniformly handle all \"located\" and node objects. A use case for this is found at: https://github.com/coq/coq/pull/485#issuecomment-287335724\r\n\r\nWe have made `'a located = t option * 'a`, removed `Loc.ghost`, and made all interfaces uniform wrt to (optional) location handling. The `'a ast` type is a private record that allows to attach extensible information to `AST` nodes.\r\n\r\nThis is interesting for base `constr` objects lack location information, so many dummy locations have to be inserted. In particular, handling of \"ghost\" locations is forced by typing now, whereas in the old case it was done in ad-hoc way, including what it seems some bugs.\r\n\r\nThe PR is a request for comments but it should be almost ready to merge. There are further improvements to be done, but I think the current point is a good compromise. Remaining tasks are:\r\n\r\n- [x] Check the test suite.\r\n - [x] Test performance, benchmarks.\r\n  - [x] Document in `doc/dev/changes.txt`\r\n- [x] Discuss/tweak the new added API in `Loc` and `CAst`.\r\n "},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/297171276","html_url":"https://github.com/coq/coq/pull/402#issuecomment-297171276","issue_url":"https://api.github.com/repos/coq/coq/issues/402","id":297171276,"user":{"login":"ejgallego","id":7192257,"avatar_url":"https://avatars1.githubusercontent.com/u/7192257?v=3","gravatar_id":"","url":"https://api.github.com/users/ejgallego","html_url":"https://github.com/ejgallego","followers_url":"https://api.github.com/users/ejgallego/followers","following_url":"https://api.github.com/users/ejgallego/following{/other_user}","gists_url":"https://api.github.com/users/ejgallego/gists{/gist_id}","starred_url":"https://api.github.com/users/ejgallego/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ejgallego/subscriptions","organizations_url":"https://api.github.com/users/ejgallego/orgs","repos_url":"https://api.github.com/users/ejgallego/repos","events_url":"https://api.github.com/users/ejgallego/events{/privacy}","received_events_url":"https://api.github.com/users/ejgallego/received_events","type":"User","site_admin":false},"created_at":"2017-04-25T21:31:46Z","updated_at":"2017-04-25T21:31:46Z","body":"Preliminary CEP open to discussion:\r\nhttps://github.com/coq/ceps/pull/19\r\nhttps://github.com/ejgallego/ceps/blob/master/text/012-coq-ml-interfaces.md"}}
{"actor":{"display_login":"ejgallego"}}