Vernacextend.OutProof
type _ t =
| No : unit t
| Close : unit t
| Update : Declare.Proof.t t
| New : Declare.Proof.t t