Merge branch 'v8.5'

1 files changed, 5 insertions, 1 deletions

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 832c08fe0e..4e889e55f0 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -644,11 +644,15 @@ module Make
             keyword (if opening then "Open " else "Close ") ++
               keyword "Scope" ++ spc() ++ str sc
           )
-        | VernacDelimiters (sc,key) ->
+        | VernacDelimiters (sc,Some key) ->
           return (
             keyword "Delimit Scope" ++ spc () ++ str sc ++
               spc() ++ keyword "with" ++ spc () ++ str key
           )
+        | VernacDelimiters (sc, None) ->
+          return (
+            keyword "Undelimit Scope" ++ spc () ++ str sc
+          )
         | VernacBindScope (sc,cll) ->
           return (
             keyword "Bind Scope" ++ spc () ++ str sc ++