Adapt to rocq-prover/rocq#21478

proux01 · proux01 · commit 9b4a4c95adff · 2026-01-08T16:40:27.000+01:00
diff --git 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.
