From 33fe6e61ff2f1f8184373ed8fccc403591c4605a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 21 Feb 2016 17:13:26 +0100
Subject: Moving the Tauto tactic to proper Ltac.

This gets rid of brittle code written in ML files through Ltac quotations, and
reduces the dependance of Coq to such a feature. This also fixes the particular
instance of bug #2800, although the underlying issue is still there.
---
 test-suite/bugs/closed/2800.v | 6 ++++++
 test-suite/bugs/opened/2800.v | 6 ------
 2 files changed, 6 insertions(+), 6 deletions(-)
 create mode 100644 test-suite/bugs/closed/2800.v
 delete mode 100644 test-suite/bugs/opened/2800.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/2800.v b/test-suite/bugs/closed/2800.v
new file mode 100644
index 0000000000..2ee438934e
--- /dev/null
+++ b/test-suite/bugs/closed/2800.v
@@ -0,0 +1,6 @@
+Goal False.
+
+intuition
+  match goal with
+  | |- _ => idtac " foo"
+  end.
diff --git a/test-suite/bugs/opened/2800.v b/test-suite/bugs/opened/2800.v
deleted file mode 100644
index c559ab0c17..0000000000
--- a/test-suite/bugs/opened/2800.v
+++ /dev/null
@@ -1,6 +0,0 @@
-Goal False.
-
-Fail intuition
-  match goal with
-  | |- _ => idtac " foo"
-  end.
-- 
cgit v1.2.3