diff options
| author | Hugo Herbelin | 2019-11-18 16:04:45 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-12-06 17:31:39 +0100 |
| commit | 490704f4b2db98f4ef15f5e380b63e49e13a418b (patch) | |
| tree | 625e60c878e2768dbce36129e1df80ceace17495 /ide | |
| parent | 28c4f57e0614523879201d1c59816cde188e5b22 (diff) | |
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.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/idetop.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |