diff options
Diffstat (limited to 'parsing/ppvernac.ml')
-rw-r--r-- | parsing/ppvernac.ml | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index a863665a9..afa28768f 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -829,9 +829,22 @@ let rec pr_vernac = function str (if List.length idl > 1 then "s " else " ") ++ prlist_with_sep spc pr_lident idl ++ str " :" ++ spc () ++ pr_lconstr c) - | VernacSetOpacity (fl,l) -> - hov 1 ((if fl then str"Opaque" else str"Transparent") ++ + | VernacSetOpacity[k,l] when k=Conv_oracle.transparent -> + hov 1 (str"Transparent" ++ spc() ++ prlist_with_sep sep pr_reference l) + | VernacSetOpacity[Conv_oracle.Opaque,l] -> + hov 1 (str"Opaque" ++ + spc() ++ prlist_with_sep sep pr_reference l) + | VernacSetOpacity l -> + let pr_lev = function + Conv_oracle.Opaque -> str"opaque" + | Conv_oracle.Expand -> str"expand" + | l when l = Conv_oracle.transparent -> str"transparent" + | Conv_oracle.Level n -> int n in + let pr_line (l,q) = + hov 2 (pr_lev l ++ spc() ++ + str"[" ++ prlist_with_sep sep pr_reference q ++ str"]") in + hov 1 (str"Strategy" ++ spc() ++ hv 0 (prlist_with_sep sep pr_line l)) | VernacUnsetOption na -> hov 1 (str"Unset" ++ spc() ++ pr_printoption na None) | VernacSetOption (na,v) -> hov 2 (str"Set" ++ spc() ++ pr_set_option na v) |