refined the conversion oracle

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10960 85f007b7-540e-0410-9357-904b9bb8a0f7

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)