Module Vernacextend.InProof
type _ t=|Ignore : unit t|Reject : unit t|Use : Declare.Proof.t t|UseOpt : Declare.Proof.t option t
val cast : Declare.Proof.t option -> 'a t -> 'a
Vernacextend.InProoftype _ t = | Ignore : unit t |
| Reject : unit t |
| Use : Declare.Proof.t t |
| UseOpt : Declare.Proof.t option t |
val cast : Declare.Proof.t option -> 'a t -> 'a