{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/285","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/285/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/285/comments","events_url":"https://api.github.com/repos/coq/coq/issues/285/events","html_url":"https://github.com/coq/coq/pull/285","id":178858373,"number":285,"title":"conversion of Strings to identifiers and back","user":{"login":"amintimany","id":5832668,"avatar_url":"https://avatars.githubusercontent.com/u/5832668?v=3","gravatar_id":"","url":"https://api.github.com/users/amintimany","html_url":"https://github.com/amintimany","followers_url":"https://api.github.com/users/amintimany/followers","following_url":"https://api.github.com/users/amintimany/following{/other_user}","gists_url":"https://api.github.com/users/amintimany/gists{/gist_id}","starred_url":"https://api.github.com/users/amintimany/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/amintimany/subscriptions","organizations_url":"https://api.github.com/users/amintimany/orgs","repos_url":"https://api.github.com/users/amintimany/repos","events_url":"https://api.github.com/users/amintimany/events{/privacy}","received_events_url":"https://api.github.com/users/amintimany/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":7,"created_at":"2016-09-23T11:57:49Z","updated_at":"2016-10-04T17:27:56Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/285","html_url":"https://github.com/coq/coq/pull/285","diff_url":"https://github.com/coq/coq/pull/285.diff","patch_url":"https://github.com/coq/coq/pull/285.patch"},"body":"This pull request adds two tactics ``ident_of_string \"id\"`` and ``string_of_ident id`` whenever the Coq module Coq.Strings.String is loaded.\r\n\r\nThe tactic ``ident_of_string \"id\"`` behaves like the ``fresh`` tactic but returns the exact identifier corresponding to the given string (Coq.Strings.String.string)``\"id\"`` (regardless of its freshness).\r\n\r\nThe tactic ``string_of_ident id`` does the exact opposite. It converts a Coq identifier to a string (Coq.Strings.String.string).\r\n\r\nThe motivation for adding these tactics is to add support for tactics like those in [Iris' ProofMode](https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/ProofMode.md) which use Coq strings to represent intro patterns to be able to convert strings to identifiers."},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/251455563","html_url":"https://github.com/coq/coq/pull/285#issuecomment-251455563","issue_url":"https://api.github.com/repos/coq/coq/issues/285","id":251455563,"user":{"login":"ppedrot","id":1202327,"avatar_url":"https://avatars.githubusercontent.com/u/1202327?v=3","gravatar_id":"","url":"https://api.github.com/users/ppedrot","html_url":"https://github.com/ppedrot","followers_url":"https://api.github.com/users/ppedrot/followers","following_url":"https://api.github.com/users/ppedrot/following{/other_user}","gists_url":"https://api.github.com/users/ppedrot/gists{/gist_id}","starred_url":"https://api.github.com/users/ppedrot/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ppedrot/subscriptions","organizations_url":"https://api.github.com/users/ppedrot/orgs","repos_url":"https://api.github.com/users/ppedrot/repos","events_url":"https://api.github.com/users/ppedrot/events{/privacy}","received_events_url":"https://api.github.com/users/ppedrot/received_events","type":"User","site_admin":false},"created_at":"2016-10-04T17:27:56Z","updated_at":"2016-10-04T17:27:56Z","body":"> How would using EXTEND ARGUMENT Help here?\r\n\r\nWell, you just define an argument whose interpretation function is the one you provide directly in the tactic AST. I can write a POC plugin for your usecase.\r\n\r\n> Otherwise I would have to bypass tactic interpretation and directly use Ftactic which I would consider very horrendous!\r\n\r\nAnd so what? All primitive intepretation functions are written in terms of `Ftactic`, so I don't see the point.\r\n\r\n> Also, I think it make sense to have a primitive tactic in the tactics AST nodes to produce an exact identifier (as opposed to a fresh identifier).\r\n\r\n*Brscmlkgrejvrtzrb!* (That was half a heart attack of mine.) This is exactly the converse!  `TacFresh` should be a primitive function, not some dedicated, ad-hoc, half-baked, non-uniform, probably bugged entry in the AST...\r\n\r\n> I understand that 8.6 is feature frozen. But is this really a feature!?\r\n\r\nErm, what would you define as a feature though? That's definitely *not* a bugfix."}}
{"actor":{"display_login":"ppedrot"}}