{"action":"opened","issue":{"url":"https://api.github.com/repos/coq/coq/issues/7092","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/7092/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/7092/comments","events_url":"https://api.github.com/repos/coq/coq/issues/7092/events","html_url":"https://github.com/coq/coq/issues/7092","id":309071112,"number":7092,"title":"Ltac matching on (co)fix should be supported","user":{"login":"JasonGross","id":396076,"avatar_url":"https://avatars0.githubusercontent.com/u/396076?v=4","gravatar_id":"","url":"https://api.github.com/users/JasonGross","html_url":"https://github.com/JasonGross","followers_url":"https://api.github.com/users/JasonGross/followers","following_url":"https://api.github.com/users/JasonGross/following{/other_user}","gists_url":"https://api.github.com/users/JasonGross/gists{/gist_id}","starred_url":"https://api.github.com/users/JasonGross/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/JasonGross/subscriptions","organizations_url":"https://api.github.com/users/JasonGross/orgs","repos_url":"https://api.github.com/users/JasonGross/repos","events_url":"https://api.github.com/users/JasonGross/events{/privacy}","received_events_url":"https://api.github.com/users/JasonGross/received_events","type":"User","site_admin":false},"labels":[{"id":723611231,"url":"https://api.github.com/repos/coq/coq/labels/kind:%20enhancement","name":"kind: enhancement","color":"0e8a16","default":false},{"id":723363885,"url":"https://api.github.com/repos/coq/coq/labels/part:%20ltac","name":"part: ltac","color":"dddddd","default":false}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2018-03-27T17:53:30Z","updated_at":"2018-03-27T17:53:30Z","closed_at":null,"author_association":"CONTRIBUTOR","body":"#### Version\r\n\r\n8.8+alpha\r\n\r\n#### Description of the problem\r\n\r\nI'd like something like this to work:\r\n```coq\r\nGoal True.\r\n  lazymatch (eval cbv delta [Nat.add] in Nat.add) with\r\n  | (fix F (n : nat) (v : ?A) {struct n} : @?P n v\r\n     := match n with\r\n        | O => @?O_case v\r\n        | S n' => @?S_case n' v (F n')\r\n        end)\r\n    => unify O_case (fun v : nat => v);\r\n         unify S_case (fun (p : nat) (m : nat) (add_p : nat -> nat)\r\n                       => S (add_p m))\r\n  end.\r\n```\r\nNote that doing it in exactly this way would require #7091, but this should also work (but is less convenient for my needs):\r\n```coq\r\nGoal True.\r\n  lazymatch (eval cbv delta [Nat.add] in Nat.add) with\r\n  | (fix F (n : nat) (v : ?A) {struct n} : @?P n v\r\n     := match n with\r\n        | O => @?O_case v\r\n        | S n' => @?S_case n' v F\r\n        end)\r\n    => unify O_case (fun v : nat => v);\r\n         unify S_case (fun (p : nat) (m : nat) (add : nat -> nat -> nat)\r\n                       => S (add p m))\r\n  end.\r\n```\r\n\r\ncc @herbelin @ppedrot "}}
{"actor":{"display_login":"JasonGross"}}