Vernacgoal (rocq-runtime.Vernacgoal)

val 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.

val pr_nth_open_subgoal : 
  ?flags:PrintingFlags.t ->
  ?oldp:Proof.t option option ->
  proof:Proof.t ->
  int ->
  Pp.t

val pr_goal_by_id : 
  ?flags:PrintingFlags.t ->
  ?oldp:Proof.t option option ->
  proof:Proof.t ->
  Libnames.qualid ->
  Pp.t

val pr_goal_emacs : 
  ?flags:PrintingFlags.t ->
  proof:Proof.t option ->
  int ->
  int ->
  Pp.t

val 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.