diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-04 14:48:24 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-04 14:48:24 +0200 |
| commit | af19d08003173718c0f7c070d0021ad958fbe58d (patch) | |
| tree | e148de88bbc70d6cd1561dffba2f301181bbb2f5 /printing | |
| parent | 90ac335a32afc6bbca5c11b7be7aabc1f7abb89b (diff) | |
| parent | 81545ec98255e644be589d34a521924549e9e2fa (diff) | |
Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 89117caf4..f26ac0bf9 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -188,7 +188,7 @@ open Pputils | ModeNoHeadEvar -> str"!" | ModeOutput -> str"-" - let pr_hint_info pr_pat { hint_priority = pri; hint_pattern = pat } = + let pr_hint_info pr_pat { Typeclasses.hint_priority = pri; hint_pattern = pat } = pr_opt (fun x -> str"|" ++ int x) pri ++ pr_opt (fun y -> (if Option.is_empty pri then str"| " else mt()) ++ pr_pat y) pat |