diff options
| author | Emilio Jesus Gallego Arias | 2020-11-15 15:57:37 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-11-18 16:25:00 +0100 |
| commit | 6aeee2e4e37d4b8ffb8c50c109903ad336c8bdfa (patch) | |
| tree | 251279a841dbae9e71126d3b1be87d2ef9bc2223 /vernac | |
| parent | ca42305f1ed1699065cffdef7d96bf5fcc0069be (diff) | |
[attributes] Update error message referring to deprecated syntax.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 2edd9d4d11..0f63dfe5ce 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -674,7 +674,7 @@ let is_polymorphic_inductive_cumulativity = let polymorphic_cumulative = let error_poly_context () = user_err - Pp.(str "The cumulative and noncumulative attributes can only be used in a polymorphic context."); + Pp.(str "The cumulative attribute can only be used in a polymorphic context."); in let open Attributes in let open Notations in |