From aac2d2ac490492f8466e1d45ba0079de376fe25a Mon Sep 17 00:00:00 2001 From: Lionel Rieg Date: Thu, 25 Jun 2015 14:58:25 +0200 Subject: Introduction of a "Undelimit Scope" command, undoing "Delimit Scope" --- printing/ppvernac.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'printing/ppvernac.ml') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 832c08fe0..4e889e55f 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 ++ -- cgit v1.2.3