From aeeeafab7f5b7424199c6de888f0adb2706f6293 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 7 Jan 2026 16:47:59 +0100 Subject: [PATCH] Adapt to https://github.com/rocq-prover/rocq/pull/21478 --- src/coqutil/Tactics/ident_ops.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/coqutil/Tactics/ident_ops.v b/src/coqutil/Tactics/ident_ops.v index a41b3a40..ca9ecab8 100644 --- a/src/coqutil/Tactics/ident_ops.v +++ b/src/coqutil/Tactics/ident_ops.v @@ -47,8 +47,8 @@ Abort. Goal forall (foo baz foobar: nat), True. intros. - pose ltac:(exact_append_ident foo bar). - assert_fails (idtac; pose ltac:(exact_append_ident foo baz)). + pose (ltac:(exact_append_ident foo bar)). + assert_fails (idtac; pose (ltac:(exact_append_ident foo baz))). Abort. Goal forall (a b c d: nat), True.