diff options
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 3b50387667..05d1086731 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -38,13 +38,11 @@ exception Redelimination let is_evaluable env ref = match ref with EvalConstRef kn -> - let (ids,kns) = Conv_oracle.freeze() in - Cpred.mem kn kns & + is_transparent (ConstKey kn) && let cb = Environ.lookup_constant kn env in cb.const_body <> None & not cb.const_opaque | EvalVarRef id -> - let (ids,sps) = Conv_oracle.freeze() in - Idpred.mem id ids & + is_transparent (VarKey id) && let (_,value,_) = Environ.lookup_named id env in value <> None |