package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type 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
module Toplevel_ : sig ... end
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