optimize_heap.v « output « test-suite - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

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

blob: e566bd7babf08c9dfeb773492b50fc3f3d93f44e (plain)

(* optimize_heap should not affect the proof state *)

Goal True.
  idtac.
  Show.
  optimize_heap.
  Show.