package coq-waterproof

  1. Overview
  2. Docs

Module WaterproofSource

Sourcemodule Backtracking : sig ... end
Sourcemodule Databases : sig ... end
Sourcemodule Exceptions : sig ... end
Sourcemodule G_waterproof : sig ... end
Sourcemodule Hint_dataset : sig ... end
Sourcemodule Hint_dataset_declarations : sig ... end
Sourcemodule Proofutils : sig ... end
Sourcemodule Waterprove : sig ... end
Sourcemodule Wp_auto : sig ... end
Sourcemodule Wp_bullets : sig ... end

This module registers two new bullet behaviors available for use in Waterproof. With

Sourcemodule Wp_eauto : sig ... end
Sourcemodule Wp_evars : sig ... end
Sourcemodule Wp_ffi : sig ... end
Sourcemodule Wp_rewrite : sig ... end