diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-31 14:24:43 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-31 14:24:43 +0000 |
| commit | dbd94e12c9c6cb0fdecb44bfedacf0c4ae50bc3e (patch) | |
| tree | f09931dac187ca9b20bb483aee7bc9beca1e78f1 /printing/prettyp.ml | |
| parent | b0631cba10fda88eb3518153860807b10441ef34 (diff) | |
Conv_orable made functional and part of pre_env
But for vm, the kernel should be functional now
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16961 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index dba047aa7..0d279c73b 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -196,14 +196,16 @@ type opacity = let opacity env = function | VarRef v when not (Option.is_empty (pi2 (Environ.lookup_named v env))) -> - Some(TransparentMaybeOpacified (Conv_oracle.get_strategy(VarKey v))) + Some(TransparentMaybeOpacified + (Conv_oracle.get_strategy (Environ.oracle env) (VarKey v))) | ConstRef cst -> let cb = Environ.lookup_constant cst env in (match cb.const_body with | Undef _ -> None | OpaqueDef _ -> Some FullyOpaque | Def _ -> Some - (TransparentMaybeOpacified (Conv_oracle.get_strategy(ConstKey cst)))) + (TransparentMaybeOpacified + (Conv_oracle.get_strategy (Environ.oracle env) (ConstKey cst)))) | _ -> None let print_opacity ref = |