diff options
| author | gareuselesinge | 2013-10-31 14:24:43 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-10-31 14:24:43 +0000 |
| commit | dbd94e12c9c6cb0fdecb44bfedacf0c4ae50bc3e (patch) | |
| tree | f09931dac187ca9b20bb483aee7bc9beca1e78f1 /pretyping/reductionops.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 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 8a614d65fd..41bd33dbcf 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -748,9 +748,10 @@ let fakey = Profile.declare_profile "fhnf_apply";; let fhnf_apply info k h a = Profile.profile4 fakey fhnf_apply info k h a;; *) -let is_transparent k = match Conv_oracle.get_strategy k with -| Conv_oracle.Opaque -> false -| _ -> true +let is_transparent e k = + match Conv_oracle.get_strategy (Environ.oracle e) k with + | Conv_oracle.Opaque -> false + | _ -> true (* Conversion utility functions *) |