optimize_heap.v « output « test-suite - coq - The formal proof system

about summary refs log tree commit diff

path: root/test-suite/output/optimize_heap.v

blob: 31b451039776dc42fc6e8029960706b9d8d74ea6 (plain)

(* optimize_heap should not affect the proof state *)

Goal True.
  idtac.
  Show.
  optimize_heap.
  Show.
Abort.