G_toplevel (coq-core.G

type vernac_toplevel =

| VernacBackTo of int

| VernacDrop

| VernacQuit

| VernacControl of Vernacexpr.vernac_control

| VernacShowGoal of {

gid : int;

sid : int;

}

| VernacShowProofDiffs of Proof_diffs.diffOpt

val err : unit -> 'a

val test_show_goal : unit Pcoq.Entry.t

val vernac_toplevel : 
  Pvernac.proof_mode option ->
  vernac_toplevel option Pcoq.Entry.t