diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2016-06-10 01:15:38 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2016-06-16 18:21:08 +0200 |
commit | 98703c8247fd86deab2d82a70c22d43797e4a548 (patch) | |
tree | f4357abeaab6a7db53419c2ed9b3c923d7d67914 /printing | |
parent | 2194292dbe88674fd9a606bb22f28d332f670f77 (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.ml | 9 |
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 |