From 81545ec98255e644be589d34a521924549e9e2fa Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 24 Apr 2018 18:46:18 +0200 Subject: [api] Move `hint_info_expr` to `Typeclasses`. `hint_info_expr`, `hint_info_gen` do conceptually belong to the typeclasses modules and should be able to be used without a dependency on the concrete vernacular syntax. --- printing/ppvernac.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 83c875707..6ad857233 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 -- cgit v1.2.3