diff --git a/tests/tactics.ref b/tests/tactics.ref
index df107d33b08b5d6b7603b8d4da31cbd82ce93e2e..be6d29675ca855115e9761fe71fab4d05652a25c 100644
--- a/tests/tactics.ref
+++ b/tests/tactics.ref
@@ -1,8 +1,6 @@
 The command has indeed failed with message:
 Failed to progress.
 The command has indeed failed with message:
-Ltac call to "destruct_or !" failed.
 Failed to progress.
 The command has indeed failed with message:
-Ltac call to "destruct_and !" failed.
 Failed to progress.