{"action":"created","issue":{"url":"https://api.github.com/repos/PrincetonUniversity/VST/issues/195","repository_url":"https://api.github.com/repos/PrincetonUniversity/VST","labels_url":"https://api.github.com/repos/PrincetonUniversity/VST/issues/195/labels{/name}","comments_url":"https://api.github.com/repos/PrincetonUniversity/VST/issues/195/comments","events_url":"https://api.github.com/repos/PrincetonUniversity/VST/issues/195/events","html_url":"https://github.com/PrincetonUniversity/VST/issues/195","id":317655734,"number":195,"title":"VST.veric.lift `_ notation conflicts with the one from Program.Util","user":{"login":"ANogin","id":1147370,"avatar_url":"https://avatars1.githubusercontent.com/u/1147370?v=4","gravatar_id":"","url":"https://api.github.com/users/ANogin","html_url":"https://github.com/ANogin","followers_url":"https://api.github.com/users/ANogin/followers","following_url":"https://api.github.com/users/ANogin/following{/other_user}","gists_url":"https://api.github.com/users/ANogin/gists{/gist_id}","starred_url":"https://api.github.com/users/ANogin/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ANogin/subscriptions","organizations_url":"https://api.github.com/users/ANogin/orgs","repos_url":"https://api.github.com/users/ANogin/repos","events_url":"https://api.github.com/users/ANogin/events{/privacy}","received_events_url":"https://api.github.com/users/ANogin/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":1,"created_at":"2018-04-25T14:33:20Z","updated_at":"2018-04-25T17:31:40Z","closed_at":null,"author_association":"NONE","body":"Not sure whether this is something worth doing anything about, but thought it may be helpful to point out.\r\n\r\nThe conflicting notations are:\r\n\r\ncoq/theories/Program/Utils.v:\r\n  ``Notation \" `  t \" := (proj1_sig t) (at level 10, t at next level) : program_scope.``\r\n\r\nVST/veric/lift.v:\r\n  ``Notation \"'`' x\" := (liftx x) (at level 9).``\r\n\r\nI noticed this when trying to use the [Coq-Equations](https://github.com/mattam82/Coq-Equations) plugin: \r\n```\r\nRequire Import floyd.proofauto.\r\nFrom Equations Require Import Equations.\r\n```\r\nresults in ``Notation ` _ is already defined at level 9 with arguments at next level while it is now required to be at level 10 with arguments at next level.`` error.\r\n"},"comment":{"url":"https://api.github.com/repos/PrincetonUniversity/VST/issues/comments/384369615","html_url":"https://github.com/PrincetonUniversity/VST/issues/195#issuecomment-384369615","issue_url":"https://api.github.com/repos/PrincetonUniversity/VST/issues/195","id":384369615,"user":{"login":"ANogin","id":1147370,"avatar_url":"https://avatars1.githubusercontent.com/u/1147370?v=4","gravatar_id":"","url":"https://api.github.com/users/ANogin","html_url":"https://github.com/ANogin","followers_url":"https://api.github.com/users/ANogin/followers","following_url":"https://api.github.com/users/ANogin/following{/other_user}","gists_url":"https://api.github.com/users/ANogin/gists{/gist_id}","starred_url":"https://api.github.com/users/ANogin/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ANogin/subscriptions","organizations_url":"https://api.github.com/users/ANogin/orgs","repos_url":"https://api.github.com/users/ANogin/repos","events_url":"https://api.github.com/users/ANogin/events{/privacy}","received_events_url":"https://api.github.com/users/ANogin/received_events","type":"User","site_admin":false},"created_at":"2018-04-25T17:31:40Z","updated_at":"2018-04-25T17:31:40Z","author_association":"NONE","body":"Yes, that would be helpful."}}
{"actor":{"display_login":"ANogin"}}