{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/9269","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/9269/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/9269/comments","events_url":"https://api.github.com/repos/coq/coq/issues/9269/events","html_url":"https://github.com/coq/coq/pull/9269","id":393610517,"node_id":"MDExOlB1bGxSZXF1ZXN0MjQwNTkyOTU1","number":9269,"title":"Move and rewrite intro pattern section","user":{"login":"jfehrle","id":1253341,"node_id":"MDQ6VXNlcjEyNTMzNDE=","avatar_url":"https://avatars1.githubusercontent.com/u/1253341?v=4","gravatar_id":"","url":"https://api.github.com/users/jfehrle","html_url":"https://github.com/jfehrle","followers_url":"https://api.github.com/users/jfehrle/followers","following_url":"https://api.github.com/users/jfehrle/following{/other_user}","gists_url":"https://api.github.com/users/jfehrle/gists{/gist_id}","starred_url":"https://api.github.com/users/jfehrle/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jfehrle/subscriptions","organizations_url":"https://api.github.com/users/jfehrle/orgs","repos_url":"https://api.github.com/users/jfehrle/repos","events_url":"https://api.github.com/users/jfehrle/events{/privacy}","received_events_url":"https://api.github.com/users/jfehrle/received_events","type":"User","site_admin":false},"labels":[{"id":661181694,"node_id":"MDU6TGFiZWw2NjExODE2OTQ=","url":"https://api.github.com/repos/coq/coq/labels/help%20wanted","name":"help wanted","color":"fff06a","default":true},{"id":649046438,"node_id":"MDU6TGFiZWw2NDkwNDY0Mzg=","url":"https://api.github.com/repos/coq/coq/labels/kind:%20documentation","name":"kind: documentation","color":"990000","default":false}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":5,"created_at":"2018-12-21T22:43:31Z","updated_at":"2018-12-24T04:21:01Z","closed_at":null,"author_association":"CONTRIBUTOR","pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/9269","html_url":"https://github.com/coq/coq/pull/9269","diff_url":"https://github.com/coq/coq/pull/9269.diff","patch_url":"https://github.com/coq/coq/pull/9269.patch"},"body":"**Kind:** documentation.\r\n\r\nFixes / closes https://github.com/coq/coq/issues/9221\r\n\r\nThis is a work in progress.  It needs a fair bit of help from those who know more.\r\n\r\nThis PR:\r\n- moves the description of intro patterns from under the intros tactic to its own subsection under \"Tactics/Invocation of tactics\"\r\n- rewrites the material almost completely to make it simpler and accessible to the non-expert.  Description progresses from the most commonly to less commonly used parts.\r\n- adds a grammar for intro patterns\r\n- adds more (and simpler) examples, grouped at the end of the section"},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/449684290","html_url":"https://github.com/coq/coq/pull/9269#issuecomment-449684290","issue_url":"https://api.github.com/repos/coq/coq/issues/9269","id":449684290,"node_id":"MDEyOklzc3VlQ29tbWVudDQ0OTY4NDI5MA==","user":{"login":"jfehrle","id":1253341,"node_id":"MDQ6VXNlcjEyNTMzNDE=","avatar_url":"https://avatars1.githubusercontent.com/u/1253341?v=4","gravatar_id":"","url":"https://api.github.com/users/jfehrle","html_url":"https://github.com/jfehrle","followers_url":"https://api.github.com/users/jfehrle/followers","following_url":"https://api.github.com/users/jfehrle/following{/other_user}","gists_url":"https://api.github.com/users/jfehrle/gists{/gist_id}","starred_url":"https://api.github.com/users/jfehrle/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jfehrle/subscriptions","organizations_url":"https://api.github.com/users/jfehrle/orgs","repos_url":"https://api.github.com/users/jfehrle/repos","events_url":"https://api.github.com/users/jfehrle/events{/privacy}","received_events_url":"https://api.github.com/users/jfehrle/received_events","type":"User","site_admin":false},"created_at":"2018-12-24T04:21:01Z","updated_at":"2018-12-24T04:21:01Z","author_association":"CONTRIBUTOR","body":"![image](https://user-images.githubusercontent.com/1253341/50390716-8e8bfc80-06ef-11e9-8115-8f939ead6084.png)\r\n\r\nSeems like the expression (syntax tree) on the second line should be more like (constr1 a1 (constr2 a2 (constr3 a3 a4)))."}}
{"actor":{"display_login":"jfehrle"}}