package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

doc/rocq-runtime.toplevel/G_toplevel/index.html

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