diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-01-08 12:47:43 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-01-08 12:47:43 +0100 |
commit | 81b57c0bffddf484a075eb1ac4911de889dd0c96 (patch) | |
tree | 9109477997495b7f69d98b004e43d0c189524bee /test-suite | |
parent | ee5d708a407d901dba61cf36451d0ac39b006522 (diff) | |
parent | c1960c794b5c8444925df67663bd70d35c67dc36 (diff) |
Merge PR #6497: Add optimize_heap tactic for #6488
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/output/optimize_heap.out | 8 | ||||
-rw-r--r-- | test-suite/output/optimize_heap.v | 7 |
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 000000000..94a0b1911 --- /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 000000000..e566bd7ba --- /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. |