From 490704f4b2db98f4ef15f5e380b63e49e13a418b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 18 Nov 2019 16:04:45 +0100
Subject: Moving the diversity of constr printers to a label style.

This allows to give access to all printing options (e.g. a scope or
being-in-context) to every printer w/o increasing the numbers of
functions.
---
 ide/idetop.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ide')

diff --git a/ide/idetop.ml b/ide/idetop.ml
index 7e55eb4d13..7d92cff365 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -196,7 +196,7 @@ let process_goal sigma g =
   let min_env = Environ.reset_context env in
   let id = Goal.uid g in
   let ccl =
-    pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g)
+    pr_letype_env ~goal_concl_style:true env sigma (Goal.V82.concl sigma g)
   in
   let process_hyp d (env,l) =
     let d' = CompactedDecl.to_named_context d in
-- 
cgit v1.2.3