{"action":"opened","issue":{"url":"https://api.github.com/repos/coq/coq/issues/6385","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/6385/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/6385/comments","events_url":"https://api.github.com/repos/coq/coq/issues/6385/events","html_url":"https://github.com/coq/coq/issues/6385","id":281085386,"number":6385,"title":"Uncaught exception CannotCoerceTo when using a tactic as an intro pattern","user":{"login":"tchajed","id":1255037,"avatar_url":"https://avatars3.githubusercontent.com/u/1255037?v=4","gravatar_id":"","url":"https://api.github.com/users/tchajed","html_url":"https://github.com/tchajed","followers_url":"https://api.github.com/users/tchajed/followers","following_url":"https://api.github.com/users/tchajed/following{/other_user}","gists_url":"https://api.github.com/users/tchajed/gists{/gist_id}","starred_url":"https://api.github.com/users/tchajed/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/tchajed/subscriptions","organizations_url":"https://api.github.com/users/tchajed/orgs","repos_url":"https://api.github.com/users/tchajed/repos","events_url":"https://api.github.com/users/tchajed/events{/privacy}","received_events_url":"https://api.github.com/users/tchajed/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2017-12-11T16:43:24Z","updated_at":"2017-12-11T16:43:24Z","closed_at":null,"author_association":"CONTRIBUTOR","body":"<!-- Thank you for your contribution.\r\n     Please complete the following information when reporting a bug. -->\r\n\r\n#### Version\r\n\r\na77f3a3e0\r\n\r\nThe Coq Proof Assistant, version 8.8+alpha (December 2017)\r\ncompiled on Dec 11 2017 9:49:14 with OCaml 4.04.2\r\n\r\n#### Operating system\r\n\r\nmacOS\r\n\r\n#### Description of the problem\r\n\r\nThe following results in `Anomaly\r\n\"Uncaught exception Ltac_plugin.Taccoerce.CannotCoerceTo(\"an introduction pattern\").\"`. It's raised by `taccoerce.ml`'s `coerce_to_intro_pattern` and uncaught by `tacinterp.ml`'s `interp_or_and_intro_pattern_option`.\r\n\r\n```coq\r\nTheorem test (A:Prop) : A \\/ A -> A.\r\n  Fail let H := idtac in intros H; destruct H as H'.\r\n  (* Disjunctive/conjunctive introduction pattern expected. *)\r\n  let H' := idtac in intros H; destruct H as H'.\r\nAbort.\r\n```"}}
{"actor":{"display_login":"tchajed"}}