{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/288","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/288/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/288/comments","events_url":"https://api.github.com/repos/coq/coq/issues/288/events","html_url":"https://github.com/coq/coq/pull/288","id":179035287,"number":288,"title":"Tentative fix for #5097 (robustness of check_evars w.r.t. \"clear\" in \"ltac:\")","user":{"login":"herbelin","id":460771,"avatar_url":"https://avatars.githubusercontent.com/u/460771?v=3","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":[{"url":"https://api.github.com/repos/coq/coq/labels/in_progress","name":"in_progress","color":"fbca04"},{"url":"https://api.github.com/repos/coq/coq/labels/needs_review","name":"needs_review","color":"d93f0b"}],"state":"closed","locked":false,"assignee":null,"assignees":[],"milestone":{"url":"https://api.github.com/repos/coq/coq/milestones/2","html_url":"https://github.com/coq/coq/milestones/8.5pl3","labels_url":"https://api.github.com/repos/coq/coq/milestones/2/labels","id":2039514,"number":2,"title":"8.5pl3","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":2,"closed_issues":4,"state":"open","created_at":"2016-09-30T07:24:22Z","updated_at":"2016-10-20T18:23:18Z","due_on":null,"closed_at":null},"comments":5,"created_at":"2016-09-24T15:23:03Z","updated_at":"2016-10-20T18:23:18Z","closed_at":"2016-10-20T18:23:18Z","pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/288","html_url":"https://github.com/coq/coq/pull/288","diff_url":"https://github.com/coq/coq/pull/288.diff","patch_url":"https://github.com/coq/coq/pull/288.patch"},"body":"This is a tentative fix for #5097, relative to a delicate topic, namely tracing the status of evars.\r\n\r\nIf a clear on an evar is executed in a term defined by \"ltac:\" (but I guess this can also arrive if evar restriction is used in regular type inference), an new restricted evar is created.\r\n\r\nThis evar was not recognized as a descendent of an existing evar but as a new unresolved evar, making the \"ltac:\" call to fail.\r\n\r\nThe patch fixes the issue by tracing pre-existing along the \"cleared\" flag, but I suspect similar treatments should be done for refining along e.g. \"change\", \"rename\" and \"move\". Is that all? Is it a correct view that an evar remains the \"same\" as another evar iff it is modified along the conversion, weakening, exchange rules?\r\n\r\nIt seems also to be indirectly related to the discussion on Qed on coqdev (Guillaume's message): how to trace shelf and given_up along similar evar restrictions. For instance, if I try to trace the evars of the shelf and given_up in Proof.run_tactic, then it seems to work well except that there are extra evars from the \"retrieved\" field. Can an expert explain the role of this \"retrieved\"? For instance, can it be removed safely if we instead trace the evars along the cleared flag?\r\n\r\n"},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/255187400","html_url":"https://github.com/coq/coq/pull/288#issuecomment-255187400","issue_url":"https://api.github.com/repos/coq/coq/issues/288","id":255187400,"user":{"login":"herbelin","id":460771,"avatar_url":"https://avatars.githubusercontent.com/u/460771?v=3","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},"created_at":"2016-10-20T18:23:18Z","updated_at":"2016-10-20T18:23:18Z","body":"Committed (which is btw not exclusive of further refinements)."}}
{"actor":{"display_login":"herbelin"}}