aboutsummaryrefslogtreecommitdiff
path: root/src/Util
diff options
context:
space:
mode:
Diffstat (limited to 'src/Util')
-rw-r--r--src/Util/Tactics/CPSId.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/Tactics/CPSId.v b/src/Util/Tactics/CPSId.v
index a7672ca51..076eed95a 100644
--- a/src/Util/Tactics/CPSId.v
+++ b/src/Util/Tactics/CPSId.v
@@ -2,7 +2,7 @@
Ltac ensure_complex_continuation allow_option k :=
lazymatch k with
- | id => fail
+ | @id _ => fail
| (fun x => x) => fail
| _
=> lazymatch allow_option with