Strategy commands are now exported

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

3 files changed, 23 insertions, 14 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 27f80fd75d..437ef58fdb 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -447,12 +447,15 @@ GEXTEND Gram
   gallina_ext:
     [ [ (* Transparent and Opaque *)
         IDENT "Transparent"; l = LIST1 global ->
-          VernacSetOpacity [Conv_oracle.transparent,l]
+          VernacSetOpacity (true,[Conv_oracle.transparent,l])
       | IDENT "Opaque"; l = LIST1 global ->
-          VernacSetOpacity [Conv_oracle.Opaque, l]
+          VernacSetOpacity (true,[Conv_oracle.Opaque, l])
       | IDENT "Strategy"; l =
           LIST1 [ lev=strategy_level; "["; q=LIST1 global; "]" -> (lev,q)] ->
-            VernacSetOpacity l
+            VernacSetOpacity (false,l)
+      | IDENT "Local"; IDENT "Strategy"; l =
+          LIST1 [ lev=strategy_level; "["; q=LIST1 global; "]" -> (lev,q)] ->
+            VernacSetOpacity (true,l)
       (* Canonical structure *)
       | IDENT "Canonical"; IDENT "Structure"; qid = global ->
 	  VernacCanonical qid
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index afa28768f1..c31defe094 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -829,13 +829,13 @@ 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[k,l] when k=Conv_oracle.transparent ->
+  | VernacSetOpacity(true,[k,l]) when k=Conv_oracle.transparent ->
       hov 1 (str"Transparent" ++
              spc() ++ prlist_with_sep sep pr_reference l)
-  | VernacSetOpacity[Conv_oracle.Opaque,l] ->
+  | VernacSetOpacity(true,[Conv_oracle.Opaque,l]) ->
       hov 1 (str"Opaque" ++
              spc() ++ prlist_with_sep sep pr_reference l)
-  | VernacSetOpacity l ->
+  | VernacSetOpacity (local,l) ->
       let pr_lev = function
           Conv_oracle.Opaque -> str"opaque"
         | Conv_oracle.Expand -> str"expand"
@@ -844,7 +844,8 @@ let rec pr_vernac = function
       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))
+      hov 1 (pr_locality local ++ 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 dc242e8caa..bdbd74b0f7 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -112,18 +112,17 @@ let need_expansion impl ref =
 
 type opacity =
   | FullyOpaque
-  | TransparentMaybeOpacified of bool
+  | TransparentMaybeOpacified of Conv_oracle.level
 
 let opacity env = function
   | VarRef v when pi2 (Environ.lookup_named v env) <> None -> 
-      Some (TransparentMaybeOpacified 
-        (not (Reductionops.is_transparent(VarKey v))))
+      Some(TransparentMaybeOpacified (Conv_oracle.get_strategy(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
-        (not(Reductionops.is_transparent(ConstKey cst))))
+      else Some
+        (TransparentMaybeOpacified (Conv_oracle.get_strategy(ConstKey cst)))
   | _ -> None
 
 let print_opacity ref =
@@ -132,8 +131,14 @@ let print_opacity ref =
     | Some s -> pr_global ref ++ str " is " ++ 
         str (match s with
           | FullyOpaque -> "opaque"
-          | TransparentMaybeOpacified true -> "basically transparent but considered opaque for reduction"
-          | TransparentMaybeOpacified false -> "transparent") ++ fnl()
+          | TransparentMaybeOpacified Conv_oracle.Opaque ->
+              "basically transparent but considered opaque for reduction"
+          | TransparentMaybeOpacified lev when lev = Conv_oracle.transparent ->
+              "transparent"
+          | TransparentMaybeOpacified (Conv_oracle.Level n) ->
+              "transparent (with expansion weight "^string_of_int n^")"
+          | TransparentMaybeOpacified Conv_oracle.Expand ->
+              "transparent (with minimal expansion weight)") ++ fnl()
     
 let print_name_infos ref =
   let impl = implicits_of_global ref in