diff options
| author | barras | 2008-05-22 17:12:11 +0000 |
|---|---|---|
| committer | barras | 2008-05-22 17:12:11 +0000 |
| commit | 9bf1f84def4e7635dd5b81038e5d76ee2a77204e (patch) | |
| tree | 4ac2cf352a6daf61f8efe70c658e3980a52c93af /parsing/prettyp.ml | |
| parent | 96876c750e05108e07dc1f29fa8db53f35f62f95 (diff) | |
Strategy commands are now exported
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10971 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/prettyp.ml')
| -rw-r--r-- | parsing/prettyp.ml | 19 |
1 files changed, 12 insertions, 7 deletions
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 |