diff options
| author | Pierre-Marie Pédrot | 2020-11-02 13:02:14 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-02 13:02:14 +0100 |
| commit | e4575cb8e80d1cb8b65dc349e4f98432e8bda523 (patch) | |
| tree | 47e5977eeb3677a9e94a98bb9add2f1dd2bbe030 /printing/printer.mli | |
| parent | a392b0225a606b6c8fe0051f0d301d5f3b6d5cd3 (diff) | |
| parent | 05f8308dbed75ee223b4d0818f1604072cffe671 (diff) | |
Merge PR #13145: Adding support for printing goal names in CoqIDE
Ack-by: Zimmi48
Reviewed-by: ppedrot
Diffstat (limited to 'printing/printer.mli')
| -rw-r--r-- | printing/printer.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/printing/printer.mli b/printing/printer.mli index a25cbebe91..ea388ae57e 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -264,3 +264,6 @@ val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t val pr_goal_emacs : proof:Proof.t option -> int -> int -> Pp.t val pr_typing_flags : Declarations.typing_flags -> Pp.t + +(** Tells if flag "Printing Goal Names" is activated *) +val print_goal_names : unit -> bool |