Library Waterproof.Waterproof


From Ltac2 Require Import Init.
Declare ML Module "waterproof:coq-waterproof.plugin".