From c3dcb5ac72bd33ffa24e0fa64ff3293135267fdd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 4 Oct 2020 23:03:37 +0200
Subject: Adding support for printing goal names in CoqIDE.

Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
Co-authored-by: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
---
 printing/printer.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index be1cc0d64a..ea718526de 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -45,6 +45,8 @@ let should_gname =
     ~key:["Printing";"Goal";"Names"]
     ~value:false
 
+let print_goal_names = should_gname (* for export *)
+
 (**********************************************************************)
 (** Terms                                                             *)
 
-- 
cgit v1.2.3