diff options
| author | Emilio Jesus Gallego Arias | 2020-05-22 03:36:36 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-26 18:28:08 +0200 |
| commit | e1a3216700427853bd5fba36e84da78b46b6cea0 (patch) | |
| tree | 1cfae455f1f70ac6f10a2577a417088571ece551 | |
| parent | d9d4dcb41d8a63b7d535200b68bcbef4a38993df (diff) | |
[declare] Nit on errors.
| -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 |