Module G_toplevel

type vernac_toplevel =
  1. | VernacBackTo of int
  2. | VernacDrop
  3. | VernacQuit
  4. | VernacControl of Vernacexpr.vernac_control
  5. | VernacShowGoalAt of {
    1. gid : int;
    2. sid : int;
    }
  6. | VernacShowGoal of Vernacexpr.goal_reference
  7. | VernacShowProofDiffs of Proof_diffs.diffOpt
val test_show_goal : unit Procq.Entry.t
val vernac_toplevel : Pvernac.proof_mode option -> vernac_toplevel option Procq.Entry.t