{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/198","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/198/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/198/comments","events_url":"https://api.github.com/repos/coq/coq/issues/198/events","html_url":"https://github.com/coq/coq/pull/198","id":159402817,"number":198,"title":"Printing of unification constraints","user":{"login":"mattam82","id":98373,"avatar_url":"https://avatars.githubusercontent.com/u/98373?v=3","gravatar_id":"","url":"https://api.github.com/users/mattam82","html_url":"https://github.com/mattam82","followers_url":"https://api.github.com/users/mattam82/followers","following_url":"https://api.github.com/users/mattam82/following{/other_user}","gists_url":"https://api.github.com/users/mattam82/gists{/gist_id}","starred_url":"https://api.github.com/users/mattam82/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mattam82/subscriptions","organizations_url":"https://api.github.com/users/mattam82/orgs","repos_url":"https://api.github.com/users/mattam82/repos","events_url":"https://api.github.com/users/mattam82/events{/privacy}","received_events_url":"https://api.github.com/users/mattam82/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":11,"created_at":"2016-06-09T13:04:42Z","updated_at":"2016-06-09T18:46:02Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/198","html_url":"https://github.com/coq/coq/pull/198","diff_url":"https://github.com/coq/coq/pull/198.diff","patch_url":"https://github.com/coq/coq/pull/198.patch"},"body":"Add an option (by default activated except in <= 8.5 compatibility mode) to print pending unification constraints in proof mode, which allows in particular to understand error messages mentioning them better."},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/224989587","html_url":"https://github.com/coq/coq/pull/198#issuecomment-224989587","issue_url":"https://api.github.com/repos/coq/coq/issues/198","id":224989587,"user":{"login":"aspiwack","id":1413217,"avatar_url":"https://avatars.githubusercontent.com/u/1413217?v=3","gravatar_id":"","url":"https://api.github.com/users/aspiwack","html_url":"https://github.com/aspiwack","followers_url":"https://api.github.com/users/aspiwack/followers","following_url":"https://api.github.com/users/aspiwack/following{/other_user}","gists_url":"https://api.github.com/users/aspiwack/gists{/gist_id}","starred_url":"https://api.github.com/users/aspiwack/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/aspiwack/subscriptions","organizations_url":"https://api.github.com/users/aspiwack/orgs","repos_url":"https://api.github.com/users/aspiwack/repos","events_url":"https://api.github.com/users/aspiwack/events{/privacy}","received_events_url":"https://api.github.com/users/aspiwack/received_events","type":"User","site_admin":false},"created_at":"2016-06-09T18:46:02Z","updated_at":"2016-06-09T18:46:02Z","body":"Additional thoughts: I question the need of a compatibility option for something that adds stuff to goal display. Considering the use of coqtop it is reasonable to just print the constraints by default. Interfaces can filter the message (by ignoring them if they use the protocol, or via regexp in the case of Proof General) if it is deemed distracting.\r\n\r\nAt any rate, there is no reason not to send the unification problem via the protocol so this option would only control coqtop and Proof General (for now)."}}
{"actor":{"display_login":"aspiwack"}}