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