diff options
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 7613cd6df..2a74ede72 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -33,7 +33,7 @@ let set_transparent_const sp = if cb.const_body <> None & cb.const_opaque then errorlabstrm "set_transparent_const" (str "Cannot make" ++ spc () ++ - Nametab.pr_global_env None (ConstRef sp) ++ + Nametab.pr_global_env Idset.empty (ConstRef sp) ++ spc () ++ str "transparent because it was declared opaque."); Conv_oracle.set_transparent_const sp |