aboutsummaryrefslogtreecommitdiff
path: root/printing/printer.ml
diff options
context:
space:
mode:
Diffstat (limited to 'printing/printer.ml')
-rw-r--r--printing/printer.ml2
1 files changed, 1 insertions, 1 deletions
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 =