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 (6)

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.3.0.tar.gz
sha256=3f0fc283e8644394aa9c7a6e3995b6d9ebbe1e6dda712bf431f9c372dcef95ad

doc/rocq-runtime.vernac/Vernacgoal/index.html

Module VernacgoalSource

Proofs, these functions obey Hyps Limit and Compact contexts.

Sourceval pr_open_subgoals : ?quiet:bool -> ?oldp:Proof.t option option -> ?flags:PrintingFlags.t -> Proof.t -> Pp.t

pr_open_subgoals ~quiet ?oldp proof shows the context for proof as used by, for example, coqtop. The first active goal is printed with all its antecedents and the conclusion. The other active goals only show their conclusions. If oldp is Some oproof, highlight the differences between the old proof oproof, and proof. quiet disables printing messages as Feedback.

Sourceval pr_nth_open_subgoal : ?flags:PrintingFlags.t -> ?oldp:Proof.t option option -> proof:Proof.t -> int -> Pp.t
Sourceval pr_goal_by_id : ?flags:PrintingFlags.t -> ?oldp:Proof.t option option -> proof:Proof.t -> Libnames.qualid -> Pp.t
Sourceval pr_goal_emacs : ?flags:PrintingFlags.t -> proof:Proof.t option -> int -> int -> Pp.t
Sourceval print_goal_name : Evd.evar_map -> Evar.t -> bool

Tells if goal name should be printed, i.e., either "Printing Goal Names" flag is activated, or the evar was given a name.