From 29343dfaa69b08f06bd949c49b0024924c40f610 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 15 Sep 2014 19:16:23 +0200
Subject: Not printing goal name (reinstalled by mistake in a previous commit).

---
 printing/printer.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/printing/printer.ml b/printing/printer.ml
index 9f6e2d667e..3264c93a5b 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -392,7 +392,7 @@ let pr_goal_tag g =
   let s = " (ID " ^ Goal.uid g ^ ")" in
   str (emacs_str s)
 
-let display_name = true
+let display_name = false
 
 (* display a goal name *)
 let pr_goal_name sigma g =
-- 
cgit v1.2.3