{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/7186","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/7186/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/7186/comments","events_url":"https://api.github.com/repos/coq/coq/issues/7186/events","html_url":"https://github.com/coq/coq/pull/7186","id":311892567,"node_id":"MDExOlB1bGxSZXF1ZXN0MTc5ODg2MDUz","number":7186,"title":"Moving `fold_constr_with_full_binders` to a place","user":{"login":"herbelin","id":460771,"node_id":"MDQ6VXNlcjQ2MDc3MQ==","avatar_url":"https://avatars1.githubusercontent.com/u/460771?v=4","gravatar_id":"","url":"https://api.github.com/users/herbelin","html_url":"https://github.com/herbelin","followers_url":"https://api.github.com/users/herbelin/followers","following_url":"https://api.github.com/users/herbelin/following{/other_user}","gists_url":"https://api.github.com/users/herbelin/gists{/gist_id}","starred_url":"https://api.github.com/users/herbelin/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/herbelin/subscriptions","organizations_url":"https://api.github.com/users/herbelin/orgs","repos_url":"https://api.github.com/users/herbelin/repos","events_url":"https://api.github.com/users/herbelin/events{/privacy}","received_events_url":"https://api.github.com/users/herbelin/received_events","type":"User","site_admin":false},"labels":[{"id":485985791,"node_id":"MDU6TGFiZWw0ODU5ODU3OTE=","url":"https://api.github.com/repos/coq/coq/labels/kind:%20cleanup","name":"kind: cleanup","color":"3366ff","default":false}],"state":"closed","locked":false,"assignee":{"login":"maximedenes","id":647105,"node_id":"MDQ6VXNlcjY0NzEwNQ==","avatar_url":"https://avatars1.githubusercontent.com/u/647105?v=4","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},"assignees":[{"login":"maximedenes","id":647105,"node_id":"MDQ6VXNlcjY0NzEwNQ==","avatar_url":"https://avatars1.githubusercontent.com/u/647105?v=4","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}],"milestone":{"url":"https://api.github.com/repos/coq/coq/milestones/16","html_url":"https://github.com/coq/coq/milestone/16","labels_url":"https://api.github.com/repos/coq/coq/milestones/16/labels","id":3512681,"node_id":"MDk6TWlsZXN0b25lMzUxMjY4MQ==","number":16,"title":"8.10+beta1","description":"","creator":{"login":"Zimmi48","id":1108325,"node_id":"MDQ6VXNlcjExMDgzMjU=","avatar_url":"https://avatars2.githubusercontent.com/u/1108325?v=4","gravatar_id":"","url":"https://api.github.com/users/Zimmi48","html_url":"https://github.com/Zimmi48","followers_url":"https://api.github.com/users/Zimmi48/followers","following_url":"https://api.github.com/users/Zimmi48/following{/other_user}","gists_url":"https://api.github.com/users/Zimmi48/gists{/gist_id}","starred_url":"https://api.github.com/users/Zimmi48/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Zimmi48/subscriptions","organizations_url":"https://api.github.com/users/Zimmi48/orgs","repos_url":"https://api.github.com/users/Zimmi48/repos","events_url":"https://api.github.com/users/Zimmi48/events{/privacy}","received_events_url":"https://api.github.com/users/Zimmi48/received_events","type":"User","site_admin":false},"open_issues":100,"closed_issues":192,"state":"open","created_at":"2018-07-20T18:48:13Z","updated_at":"2018-10-26T12:01:32Z","due_on":null,"closed_at":null},"comments":17,"created_at":"2018-04-06T08:39:34Z","updated_at":"2018-10-26T12:06:47Z","closed_at":"2018-10-26T09:08:42Z","author_association":"MEMBER","pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/7186","html_url":"https://github.com/coq/coq/pull/7186","diff_url":"https://github.com/coq/coq/pull/7186.diff","patch_url":"https://github.com/coq/coq/pull/7186.patch"},"body":"**Kind:** cleanup\r\n\r\n~~Was dependent on #7080 which is now merged.~~\r\n\r\nAt the time of introducing `EConstr`, `Termops` naturally became a file mainly working on `econstr` (i.e. morally an `econstrops.ml` file). So, `Termops.fold_constr_with_full_binders` there, moved to a version taking an `econstr` as argument.\r\n\r\nHowever, the file `assumptions.ml` was still needing a variant of `fold_constr_with_full_binders` on `constr` even though the file was high in the hierarchy, so, a copy of `fold_constr_with_full_binders` was duplicated there.\r\n\r\nFor the purpose of code factorization, for the purpose of organizing the code on \"libraries\" about datatypes, this PR moved this local copy of `fold_constr_with_full_binders` in `constr.ml` which is the place where, I believe, it morally lives.\r\n\r\nThe drawback is that it makes the kernel size \"bigger\" (in the sense of providing utilities which are not strictly necessary for kernel type-checking). But I feel that the consensus is more in the direction of taking advantage of centralized code than, as it was the case at some time, to take advantage of a reduced kernel about which we know exactly what is needed. After all, for the purpose of knowing the minimal amount of functions needed for type-checking, it seems to me that we can consider that the checker is a better place. [An alternative would be otherwise to keep a `constrops.ml` copy besides `termops.ml` outside of the kernel.]\r\n\r\nNote that the `with_full_binders` combinators needs `Context`, so this is another reason why it is interesting to have `Context` coming before `Constr` (or conversely, to have combinators on `constr` defined after contexts are defined)."},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/433385844","html_url":"https://github.com/coq/coq/pull/7186#issuecomment-433385844","issue_url":"https://api.github.com/repos/coq/coq/issues/7186","id":433385844,"node_id":"MDEyOklzc3VlQ29tbWVudDQzMzM4NTg0NA==","user":{"login":"Zimmi48","id":1108325,"node_id":"MDQ6VXNlcjExMDgzMjU=","avatar_url":"https://avatars2.githubusercontent.com/u/1108325?v=4","gravatar_id":"","url":"https://api.github.com/users/Zimmi48","html_url":"https://github.com/Zimmi48","followers_url":"https://api.github.com/users/Zimmi48/followers","following_url":"https://api.github.com/users/Zimmi48/following{/other_user}","gists_url":"https://api.github.com/users/Zimmi48/gists{/gist_id}","starred_url":"https://api.github.com/users/Zimmi48/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Zimmi48/subscriptions","organizations_url":"https://api.github.com/users/Zimmi48/orgs","repos_url":"https://api.github.com/users/Zimmi48/repos","events_url":"https://api.github.com/users/Zimmi48/events{/privacy}","received_events_url":"https://api.github.com/users/Zimmi48/received_events","type":"User","site_admin":false},"created_at":"2018-10-26T12:06:47Z","updated_at":"2018-10-26T12:06:47Z","author_association":"MEMBER","body":"Even though this particular failure was spurious, it also means that none of the tests in the following stage did run. Thus, it should preferably have been restarted instead of being ignored."}}
{"actor":{"display_login":"Zimmi48"}}