aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2016-04-04 14:49:06 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2016-04-04 14:49:06 +0200
commit16536fd734d6a7aaa6ff85f56cef629df74ce36a (patch)
treea9ffc8d0830c7c826ea164b5267f95985365fe63 /printing
parent5569a06d062f913c66cbcb8bd01d4505e603d321 (diff)
parent6aa58955515dff338ea85d59073dfc0d0c7648ab (diff)
Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into JasonGross-trunk-function_scope
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