aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Armaël Guéneau <armael.gueneau@ens-lyon.fr>2018-05-31 17:53:51 +0200
committerGravatar Armaël Guéneau <armael.gueneau@ens-lyon.fr>2018-05-31 17:53:51 +0200
commit8f712ae36be438abca49756d0fe3bb95c428a91e (patch)
tree6a872d0ddc04e3adf6a50563dead153ac077cb04
parentac8a84e3b4dc530b000e17b72c7e26f7a957420f (diff)
Fix a couple typos in deprecation messages
-rw-r--r--vernac/vernacexpr.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 4ff9d105b..c9b41ecbe 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -106,13 +106,13 @@ type comment =
type reference_or_constr = Hints.reference_or_constr =
| HintsReference of reference
| HintsConstr of constr_expr
-[@@ocaml.deprecated "Please use [Hints.hints_expr]"]
+[@@ocaml.deprecated "Please use [Hints.reference_or_constr]"]
type hint_mode = Hints.hint_mode =
| ModeInput (* No evars *)
| ModeNoHeadEvar (* No evar at the head *)
| ModeOutput (* Anything *)
-[@@ocaml.deprecated "Please use [Hints.hints_expr]"]
+[@@ocaml.deprecated "Please use [Hints.hint_mode]"]
type 'a hint_info_gen = 'a Typeclasses.hint_info_gen =
{ hint_priority : int option;