Module G_toplevel
type vernac_toplevel
=
|
VernacBacktrack of int * int * int
|
VernacDrop
|
VernacQuit
|
VernacControl of Vernacexpr.vernac_control
module Toplevel_ : sig ... end
val vernac_toplevel : Pvernac.proof_mode option -> vernac_toplevel CAst.t option Pcoq.Entry.t