Skip to content
Snippets Groups Projects
Commit 49b8abe5 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'patch-1' into 'master'

tactics.v: Fix parsing precedence for `select` tactic

See merge request iris/stdpp!157
parents 432120a3 6eb05dfc
No related branches found
No related tags found
1 merge request!157tactics.v: Fix parsing precedence for `select` tactic
Pipeline #27749 passed
......@@ -531,7 +531,7 @@ matching hypotheses.
[select] is written in CPS and does not return the name of the
hypothesis due to limitations in the Ltac1 tactic runtime (see
https://gitter.im/coq/coq?at=5e96c82f85b01628f04bbb89). *)
Tactic Notation "select" open_constr(pat) tactic(tac) :=
Tactic Notation "select" open_constr(pat) tactic3(tac) :=
lazymatch goal with
(* The [unify] is necessary, otherwise holes in [pat] stay as side-conditions *)
| H : pat |- _ => let T := (type of H) in unify T pat; tac H
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment