diff options
| -rw-r--r-- | vernac/declare.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/declare.ml b/vernac/declare.ml index 65f0265b3e..5be819e109 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -1266,8 +1266,8 @@ let not_transp_msg = ++ spc () ++ str "Use 'Defined' instead.") -let pperror cmd = CErrors.user_err ~hdr:"Program" cmd -let err_not_transp () = pperror not_transp_msg +let err_not_transp () = + CErrors.user_err ~hdr:"Program" not_transp_msg module ProgMap = Id.Map |