package rocq-runtime

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

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.