package rocq-runtime

  1. Overview
  2. Docs
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module G_toplevelSource

Sourcetype vernac_toplevel =
  1. | VernacBackTo of int
  2. | VernacDrop
  3. | VernacQuit
  4. | VernacControl of Vernacexpr.vernac_control
  5. | VernacShowGoal of {
    1. gid : int;
    2. sid : int;
    }
  6. | VernacShowProofDiffs of Proof_diffs.diffOpt
Sourceval err : unit -> 'a
Sourceval test_show_goal : unit Procq.Entry.t
Sourceval vernac_toplevel : Pvernac.proof_mode option -> vernac_toplevel option Procq.Entry.t