diff options
Diffstat (limited to 'proofs/redexpr.ml')
| -rw-r--r-- | proofs/redexpr.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 69ef4598d..c6b3339d7 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -38,12 +38,13 @@ let set_strategy_one ref l = Csymtable.set_opaque_const sp | ConstKey sp, _ -> let cb = Global.lookup_constant sp in - if cb.const_body <> None & cb.const_opaque then - errorlabstrm "set_transparent_const" - (str "Cannot make" ++ spc () ++ - Nametab.pr_global_env Idset.empty (ConstRef sp) ++ - spc () ++ str "transparent because it was declared opaque."); - Csymtable.set_transparent_const sp + (match cb.const_body with + | OpaqueDef _ -> + errorlabstrm "set_transparent_const" + (str "Cannot make" ++ spc () ++ + Nametab.pr_global_env Idset.empty (ConstRef sp) ++ + spc () ++ str "transparent because it was declared opaque."); + | _ -> Csymtable.set_transparent_const sp) | _ -> () let cache_strategy (_,str) = |