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. --- plugins/ltac/extratactics.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index a5f8060ae..797dfbe23 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -315,7 +315,7 @@ let project_hint ~poly pri l2r r = let ctx = Evd.const_univ_entry ~poly sigma in let c = EConstr.to_constr sigma c in let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in - let info = {Vernacexpr.hint_priority = pri; hint_pattern = None} in + let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in (info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c)) let add_hints_iff ~atts l2r lc n bl = -- cgit v1.2.3