aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--vernac/ppvernac.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 00a5727af6..01873918aa 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -271,9 +271,9 @@ let pr_reference_or_constr pr_c = function
| HintsConstr c -> pr_c c
let pr_hint_mode = let open Hints in function
- | ModeInput -> str"+"
- | ModeNoHeadEvar -> str"!"
- | ModeOutput -> str"-"
+ | ModeInput -> str"+"
+ | ModeNoHeadEvar -> str"!"
+ | ModeOutput -> str"-"
let pr_hint_info pr_pat { Typeclasses.hint_priority = pri; hint_pattern = pat } =
pr_opt (fun x -> str"|" ++ int x) pri ++