diff options
Diffstat (limited to 'toplevel/vernac.ml')
| -rw-r--r-- | toplevel/vernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 7e81aa20a..a61ade784 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -29,7 +29,7 @@ let checknav_deep (loc, ast) = let disable_drop = function - | Drop -> CErrors.error "Drop is forbidden." + | Drop -> CErrors.user_err Pp.(str "Drop is forbidden.") | e -> e (* Echo from a buffer based on position. |