add optimize_heap tactic for #6488

2 files changed, 15 insertions, 0 deletions

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.