From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 16 Jun 2006 14:41:51 +0000
Subject: Imported Upstream version 8.0pl3+8.1beta

---
 test-suite/output/Tactics.out | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'test-suite/output/Tactics.out')

diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out
index 71c59e43..8e8b8059 100644
--- a/test-suite/output/Tactics.out
+++ b/test-suite/output/Tactics.out
@@ -1 +1,4 @@
 intro H; split; [  a H |  e H ].
+intros; match goal with
+        | |- context [if ?X then _ else _] => case X
+        end; trivial.
-- 
cgit v1.2.3