aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/ppvernac.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index c1f5e122b..55f8f909f 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -648,7 +648,7 @@ module Make
| VernacBindScope (sc,cll) ->
return (
keyword "Bind Scope" ++ spc () ++ str sc ++
- spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_smart_global cll
+ spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_class_rawexpr cll
)
| VernacArgumentsScope (q,scl) ->
let pr_opt_scope = function