{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/185","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/185/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/185/comments","events_url":"https://api.github.com/repos/coq/coq/issues/185/events","html_url":"https://github.com/coq/coq/pull/185","id":157943063,"number":185,"title":"Remove unused print tagging infrastructure","user":{"login":"ejgallego","id":7192257,"avatar_url":"https://avatars.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":396673733,"url":"https://api.github.com/repos/coq/coq/labels/redesign","name":"redesign","color":"fef2c0","default":false}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":{"url":"https://api.github.com/repos/coq/coq/milestones/3","html_url":"https://github.com/coq/coq/milestones/8.7","labels_url":"https://api.github.com/repos/coq/coq/milestones/3/labels","id":2046481,"number":3,"title":"8.7","description":"","creator":{"login":"maximedenes","id":647105,"avatar_url":"https://avatars.githubusercontent.com/u/647105?v=3","gravatar_id":"","url":"https://api.github.com/users/maximedenes","html_url":"https://github.com/maximedenes","followers_url":"https://api.github.com/users/maximedenes/followers","following_url":"https://api.github.com/users/maximedenes/following{/other_user}","gists_url":"https://api.github.com/users/maximedenes/gists{/gist_id}","starred_url":"https://api.github.com/users/maximedenes/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/maximedenes/subscriptions","organizations_url":"https://api.github.com/users/maximedenes/orgs","repos_url":"https://api.github.com/users/maximedenes/repos","events_url":"https://api.github.com/users/maximedenes/events{/privacy}","received_events_url":"https://api.github.com/users/maximedenes/received_events","type":"User","site_admin":false},"open_issues":15,"closed_issues":0,"state":"open","created_at":"2016-10-04T11:18:56Z","updated_at":"2016-11-21T15:49:27Z","due_on":null,"closed_at":null},"comments":28,"created_at":"2016-06-01T15:53:25Z","updated_at":"2016-12-06T17:14:02Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/185","html_url":"https://github.com/coq/coq/pull/185","diff_url":"https://github.com/coq/coq/pull/185.diff","patch_url":"https://github.com/coq/coq/pull/185.patch"},"body":"This PR removes the functorial-based tagging parametrization printers. It also removes unused \"generic\" tags.\n\nPrinters now tag unconditionally, and it is up to the backends to interpret tags.\n\nThe motivation for this PR is:\n- The full capabilities of the API were not used, the intended use case was not clear.\n- It made printers more complex, but extensiblity still depended on manual modification of printers.\n- Unused `Ppannotation` confused people as what its purpose was.\n\nThe PR is split in two patches. The first one removes the functors, the second initiates a rework of tagging.\n\nFuture work is to sync the notion of rich document and tags.\n\nTested, test-suite passes, colors work, saves 24K of bytecode.\n\nNotes:\n- We have also removed the `Richprinter` module. It was only used in the `annotate` IDE protocol call, its output was identical to the normal printer (or even inconsistent if taggers were not kept manually in\n  sync).\n- Note that Richpp didn't need a single change for the first part. This is due as its main API entry point `Richpp.rich_pp` is not used by anyone.\n"},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/265210539","html_url":"https://github.com/coq/coq/pull/185#issuecomment-265210539","issue_url":"https://api.github.com/repos/coq/coq/issues/185","id":265210539,"user":{"login":"ejgallego","id":7192257,"avatar_url":"https://avatars.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":"2016-12-06T17:14:02Z","updated_at":"2016-12-06T17:14:02Z","body":"Superseded by #390 "}}
{"actor":{"display_login":"ejgallego"}}