From 924d085e30090b2c1ff943ed67ef86828e78f104 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 28 Feb 2020 13:40:28 +0100
Subject: [PATCH] Fix test in Coq 8.10 and 8.11.

---
 tests/tactics.ref | 2 --
 1 file changed, 2 deletions(-)

diff --git a/tests/tactics.ref b/tests/tactics.ref
index df107d33..be6d2967 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.
-- 
GitLab