refined the conversion oracle

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

3 files changed, 33 insertions, 7 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 2efe88c0c3..27f80fd75d 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -446,9 +446,13 @@ GEXTEND Gram
 
   gallina_ext:
     [ [ (* Transparent and Opaque *)
-        IDENT "Transparent"; l = LIST1 global -> VernacSetOpacity (false, l)
-      | IDENT "Opaque"; l = LIST1 global -> VernacSetOpacity (true, l)
-
+        IDENT "Transparent"; l = LIST1 global ->
+          VernacSetOpacity [Conv_oracle.transparent,l]
+      | IDENT "Opaque"; l = LIST1 global ->
+          VernacSetOpacity [Conv_oracle.Opaque, l]
+      | IDENT "Strategy"; l =
+          LIST1 [ lev=strategy_level; "["; q=LIST1 global; "]" -> (lev,q)] ->
+            VernacSetOpacity l
       (* Canonical structure *)
       | IDENT "Canonical"; IDENT "Structure"; qid = global ->
 	  VernacCanonical qid
@@ -542,6 +546,13 @@ GEXTEND Gram
     [ [ ":="; l = LIST1 typeclass_field_def SEP ";" -> l
     | -> [] ] ]
   ;
+  strategy_level:
+    [ [ IDENT "expand" -> Conv_oracle.Expand
+      | IDENT "opaque" -> Conv_oracle.Opaque
+      | n=INT -> Conv_oracle.Level (int_of_string n)
+      | "-"; n=INT -> Conv_oracle.Level (- int_of_string n)
+      | IDENT "transparent" -> Conv_oracle.transparent ] ]
+  ;
 END
 
 GEXTEND Gram
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index a863665a97..afa28768f1 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)
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 6ca3a5c1a1..dc242e8caa 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -116,12 +116,14 @@ type opacity =
 
 let opacity env = function
   | VarRef v when pi2 (Environ.lookup_named v env) <> None -> 
-      Some (TransparentMaybeOpacified (Conv_oracle.is_opaque_var v))
+      Some (TransparentMaybeOpacified 
+        (not (Reductionops.is_transparent(VarKey v))))
   | ConstRef cst ->
       let cb = Environ.lookup_constant cst env in
       if cb.const_body = None then None
       else if cb.const_opaque then Some FullyOpaque
-      else Some (TransparentMaybeOpacified (Conv_oracle.is_opaque_cst cst))
+      else Some (TransparentMaybeOpacified
+        (not(Reductionops.is_transparent(ConstKey cst))))
   | _ -> None
 
 let print_opacity ref =