From c1960c794b5c8444925df67663bd70d35c67dc36 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Wed, 3 Jan 2018 14:42:52 -0500
Subject: add optimize_heap tactic for #6488

---
 test-suite/output/optimize_heap.out | 8 ++++++++
 test-suite/output/optimize_heap.v   | 7 +++++++
 2 files changed, 15 insertions(+)
 create mode 100644 test-suite/output/optimize_heap.out
 create mode 100644 test-suite/output/optimize_heap.v

(limited to 'test-suite')

diff --git a/test-suite/output/optimize_heap.out b/test-suite/output/optimize_heap.out
new file mode 100644
index 0000000000..94a0b19118
--- /dev/null
+++ b/test-suite/output/optimize_heap.out
@@ -0,0 +1,8 @@
+1 subgoal
+  
+  ============================
+  True
+1 subgoal
+  
+  ============================
+  True
diff --git a/test-suite/output/optimize_heap.v b/test-suite/output/optimize_heap.v
new file mode 100644
index 0000000000..e566bd7bab
--- /dev/null
+++ b/test-suite/output/optimize_heap.v
@@ -0,0 +1,7 @@
+(* optimize_heap should not affect the proof state *)
+
+Goal True.
+  idtac.
+  Show.
+  optimize_heap.
+  Show.
-- 
cgit v1.2.3