aboutsummaryrefslogtreecommitdiff
path: root/printing/printer.mli
diff options
context:
space:
mode:
Diffstat (limited to 'printing/printer.mli')
-rw-r--r--printing/printer.mli3
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