From dbd94e12c9c6cb0fdecb44bfedacf0c4ae50bc3e Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Thu, 31 Oct 2013 14:24:43 +0000 Subject: 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 --- printing/prettyp.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'printing/prettyp.ml') 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 = -- cgit v1.2.3