diff options
Diffstat (limited to 'proofs/redexpr.ml')
| -rw-r--r-- | proofs/redexpr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index e4b8697d1..be0cba3a1 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -44,7 +44,7 @@ let set_strategy_one ref l = | OpaqueDef _ -> errorlabstrm "set_transparent_const" (str "Cannot make" ++ spc () ++ - Nametab.pr_global_env Idset.empty (ConstRef sp) ++ + Nametab.pr_global_env Id.Set.empty (ConstRef sp) ++ spc () ++ str "transparent because it was declared opaque."); | _ -> Csymtable.set_transparent_const sp) | _ -> () |