From 083124d659fa6ca2d88c9bd9a8c64ad7b7de9224 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sun, 28 Oct 2018 14:28:39 -0400
Subject: Fix a bug in ensure_complex_continuation

---
 src/Util/Tactics/CPSId.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/Util')

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
-- 
cgit v1.2.3