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