diff options
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 2d87b51d73..f4a112a4cb 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1110,6 +1110,11 @@ module Make return ( hov 2 (keyword "Set" ++ spc() ++ pr_set_option na v) ) + | VernacSetAppendOption (na,v) -> + return ( + hov 2 (keyword "Set" ++ spc() ++ pr_printoption na None ++ + spc() ++ keyword "Append" ++ spc() ++ str v) + ) | VernacAddOption (na,l) -> return ( hov 2 (keyword "Add" ++ spc() ++ pr_printoption na (Some l)) |