aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2016-06-10 01:15:38 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2016-06-16 18:21:08 +0200
commit98703c8247fd86deab2d82a70c22d43797e4a548 (patch)
treef4357abeaab6a7db53419c2ed9b3c923d7d67914 /printing
parent2194292dbe88674fd9a606bb22f28d332f670f77 (diff)
Extend Hint Mode to handle the no-head-evar case
Suggested by R. Krebbers and C. Cohen, this makes modes more applicable, by allowing to trigger resolution on partially instantiated indices. This is a rough but fast approximation of the pattern on which one would like instances to apply.
Diffstat (limited to 'printing')
-rw-r--r--printing/ppvernac.ml9
1 files changed, 7 insertions, 2 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index f3558054b..5b73b054d 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -161,6 +161,11 @@ module Make
| HintsReference r -> pr_reference r
| HintsConstr c -> pr_c c
+ let pr_hint_mode = function
+ | ModeInput -> str"+"
+ | ModeNoHeadEvar -> str"!"
+ | ModeOutput -> str"-"
+
let pr_hints db h pr_c pr_pat =
let opth = pr_opt_hintbases db in
let pph =
@@ -182,8 +187,8 @@ module Make
| HintsMode (m, l) ->
keyword "Mode"
++ spc ()
- ++ pr_reference m ++ spc() ++ prlist_with_sep spc
- (fun b -> if b then str"+" else str"-") l
+ ++ pr_reference m ++ spc() ++
+ prlist_with_sep spc pr_hint_mode l
| HintsConstructors c ->
keyword "Constructors"
++ spc() ++ prlist_with_sep spc pr_reference c