{"action":"closed","issue":{"url":"https://api.github.com/repos/coq/coq/issues/9428","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/9428/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/9428/comments","events_url":"https://api.github.com/repos/coq/coq/issues/9428/events","html_url":"https://github.com/coq/coq/issues/9428","id":404223917,"node_id":"MDU6SXNzdWU0MDQyMjM5MTc=","number":9428,"title":"\"Locate\" lacking newlines between notations [regression]","user":{"login":"RalfJung","id":330628,"node_id":"MDQ6VXNlcjMzMDYyOA==","avatar_url":"https://avatars1.githubusercontent.com/u/330628?v=4","gravatar_id":"","url":"https://api.github.com/users/RalfJung","html_url":"https://github.com/RalfJung","followers_url":"https://api.github.com/users/RalfJung/followers","following_url":"https://api.github.com/users/RalfJung/following{/other_user}","gists_url":"https://api.github.com/users/RalfJung/gists{/gist_id}","starred_url":"https://api.github.com/users/RalfJung/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/RalfJung/subscriptions","organizations_url":"https://api.github.com/users/RalfJung/orgs","repos_url":"https://api.github.com/users/RalfJung/repos","events_url":"https://api.github.com/users/RalfJung/events{/privacy}","received_events_url":"https://api.github.com/users/RalfJung/received_events","type":"User","site_admin":false},"labels":[{"id":723364138,"node_id":"MDU6TGFiZWw3MjMzNjQxMzg=","url":"https://api.github.com/repos/coq/coq/labels/part:%20notations","name":"part: notations","color":"dddddd","default":false}],"state":"closed","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":1,"created_at":"2019-01-29T10:33:31Z","updated_at":"2019-10-18T19:28:11Z","closed_at":"2019-10-18T19:28:11Z","author_association":"CONTRIBUTOR","body":"<!-- Thank you for your contribution.\r\n     Please complete the following information when reporting a bug. -->\r\n\r\n#### Version\r\n\r\n<!-- You can get this information by running `coqtop -v`. -->\r\n8.9.0\r\n\r\n#### Operating system\r\nLinux\r\n\r\n#### Description of the problem\r\n\r\nThe following file\r\n```\r\nNotation \"b1 && b2\" := (if b1 then b2 else false).\r\nLocate \"&&\".\r\n```\r\nprints\r\n```\r\nNotation\r\n\"b1 && b2\" := if b1 then b2 else false (default interpretation)\"x && y\" := andb x y : bool_scope\r\n```\r\nAs you can see, a newline is missing between the two printed notations.\r\n\r\nThis is a recent regression, I think it still worked fine with the 8.8 series."}}
{"actor":{"display_login":"herbelin"}}