From 82b959a8f6025f84a39efb67985e6fe1a338b94b Mon Sep 17 00:00:00 2001
From: barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 21 May 2008 23:25:22 +0000
Subject: refined the conversion oracle

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10960 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/ppvernac.ml | 17 +++++++++++++++--
 1 file changed, 15 insertions(+), 2 deletions(-)

(limited to 'parsing/ppvernac.ml')

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)
-- 
cgit v1.2.3