{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/7254","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/7254/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/7254/comments","events_url":"https://api.github.com/repos/coq/coq/issues/7254/events","html_url":"https://github.com/coq/coq/pull/7254","id":314380048,"node_id":"MDExOlB1bGxSZXF1ZXN0MTgxNjc3NDg2","number":7254,"title":"Inductive params","user":{"login":"jashug","id":1844608,"node_id":"MDQ6VXNlcjE4NDQ2MDg=","avatar_url":"https://avatars2.githubusercontent.com/u/1844608?v=4","gravatar_id":"","url":"https://api.github.com/users/jashug","html_url":"https://github.com/jashug","followers_url":"https://api.github.com/users/jashug/followers","following_url":"https://api.github.com/users/jashug/following{/other_user}","gists_url":"https://api.github.com/users/jashug/gists{/gist_id}","starred_url":"https://api.github.com/users/jashug/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jashug/subscriptions","organizations_url":"https://api.github.com/users/jashug/orgs","repos_url":"https://api.github.com/users/jashug/repos","events_url":"https://api.github.com/users/jashug/events{/privacy}","received_events_url":"https://api.github.com/users/jashug/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},{"id":777223550,"node_id":"MDU6TGFiZWw3NzcyMjM1NTA=","url":"https://api.github.com/repos/coq/coq/labels/needs:%20benchmarking","name":"needs: benchmarking","color":"c2e0c6","default":false},{"id":832236574,"node_id":"MDU6TGFiZWw4MzIyMzY1NzQ=","url":"https://api.github.com/repos/coq/coq/labels/part:%20elaboration","name":"part: elaboration","color":"dddddd","default":false}],"state":"open","locked":false,"assignee":{"login":"mattam82","id":98373,"node_id":"MDQ6VXNlcjk4Mzcz","avatar_url":"https://avatars1.githubusercontent.com/u/98373?v=4","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},"assignees":[{"login":"mattam82","id":98373,"node_id":"MDQ6VXNlcjk4Mzcz","avatar_url":"https://avatars1.githubusercontent.com/u/98373?v=4","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}],"milestone":null,"comments":21,"created_at":"2018-04-15T02:42:26Z","updated_at":"2018-07-03T20:53:47Z","closed_at":null,"author_association":"CONTRIBUTOR","pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/7254","html_url":"https://github.com/coq/coq/pull/7254","diff_url":"https://github.com/coq/coq/pull/7254.diff","patch_url":"https://github.com/coq/coq/pull/7254.patch"},"body":"**Kind:** cleanup\r\nCloses #7253\r\n- [x] Entry added in CHANGES.\r\n- [x] Add test\r\n\r\nI wonder how often this is used in practice. I hope CI will show it is not used very often.\r\n\r\nLooks like this feature was last touched by @herbelin in https://github.com/coq/coq/commit/1f798216ede7e3813d75732fbebc1f8fbf6622c5"},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/402288907","html_url":"https://github.com/coq/coq/pull/7254#issuecomment-402288907","issue_url":"https://api.github.com/repos/coq/coq/issues/7254","id":402288907,"node_id":"MDEyOklzc3VlQ29tbWVudDQwMjI4ODkwNw==","user":{"login":"jashug","id":1844608,"node_id":"MDQ6VXNlcjE4NDQ2MDg=","avatar_url":"https://avatars2.githubusercontent.com/u/1844608?v=4","gravatar_id":"","url":"https://api.github.com/users/jashug","html_url":"https://github.com/jashug","followers_url":"https://api.github.com/users/jashug/followers","following_url":"https://api.github.com/users/jashug/following{/other_user}","gists_url":"https://api.github.com/users/jashug/gists{/gist_id}","starred_url":"https://api.github.com/users/jashug/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jashug/subscriptions","organizations_url":"https://api.github.com/users/jashug/orgs","repos_url":"https://api.github.com/users/jashug/repos","events_url":"https://api.github.com/users/jashug/events{/privacy}","received_events_url":"https://api.github.com/users/jashug/received_events","type":"User","site_admin":false},"created_at":"2018-07-03T20:53:47Z","updated_at":"2018-07-03T20:53:47Z","author_association":"CONTRIBUTOR","body":"Yeah, SF is related. And while I was looking into fixing it, I found this problem:\r\n```coq\r\nAxiom list : Type -> Type.\r\nAxiom nil : forall {T}, list T.\r\nAxiom inj : forall {T}, T -> list T.\r\n\r\nInductive reg_exp {T : Type} : Type :=\r\n| EmptySet : reg_exp\r\n| Char : T -> reg_exp\r\n.\r\n\r\nInductive exp_match {T} : list T -> reg_exp (T := _) -> Prop :=\r\n| MChar : forall x : _, exp_match (T := _) (inj x) (Char x)\r\n.\r\n(*\r\nCannot unify:\r\n(exp_match ?T (inj x) (Char x))\r\nwith\r\n(exp_match T ?l ?r)\r\n*)\r\n```\r\n\r\nDigging into things, we have\r\n```\r\n(ocd) p sigma_with_model_evars\r\nsigma_with_model_evars: Evd.evar_map = UNDEFINED EVARS: (+level 2 closure):\r\n   ?X6==[T |- Type@{Top.7} => ?X7@{__:=T}] (underscore)\r\n   ?X7==[T |- Type@{Top.16} => ?X15] (underscore)\r\n   ?X8==[exp_match T |- Type@{Top.16} => ?X15] (underscore)\r\n   ?X12==[exp_match T {x} |- Type@{Top.16} => ?X8@{__:=exp_match; __:=T}]\r\n           (underscore)\r\n   ?X14==[exp_match T {x} |- Type@{Top.16}\r\n           => ?X7@{__:=?X12@{__:=exp_match; __:=T}}] (parameter T of\r\n           CSTR.reg_exp._0._2)\r\n   ?X15==[{T} |- Type@{Top.16}] (underscore) {?T}\r\n   ?X16==[exp_match T x |- list T] (internal placeholder) {?l}\r\n   ?X17==[exp_match T x |- reg_exp ?X7@{__:=T}] (internal placeholder) {?zz}\r\n\r\n-- Universes elided --\r\n\r\n(ocd) p concl_env\r\nconcl_env: Environ.env = []\r\n  [(exp_match : forall (T : ?X5) (_ : list T) (_ : reg_exp ?X7@{__:=T}), Prop)\r\n  (T : ?X5) (x : ?X15)]\r\n(ocd) p model\r\nmodel: EConstr.t =\r\n  _UNBOUND_REL_3 _UNBOUND_REL_2\r\n    ?X16@{__:=_UNBOUND_REL_3; __:=_UNBOUND_REL_2; __:=_UNBOUND_REL_1}\r\n    ?X17@{__:=_UNBOUND_REL_3; __:=_UNBOUND_REL_2; __:=_UNBOUND_REL_1}\r\n(ocd) p concl\r\nconcl: EConstr.constr =\r\n  _UNBOUND_REL_3 ?X15 (inj ?X15 _UNBOUND_REL_1)\r\n    (CSTR.reg_exp._0._2 ?X15 _UNBOUND_REL_1)\r\n```\r\nand `Evarconv.conv concl_env sigma_with_model_evars concl model` returning `None`.\r\n\r\nI don't understand this: if we set `?X15 = T = Rel_2`, then set `?X16 = inj T x` and `?X17 = CSTR.reg_exp._0._2 T`, these should unify.\r\nIs there some problem with restricted evar contexts or something?"}}
{"actor":{"display_login":"jashug"}}