From 5c23e9602fd5d74f748b8b6c5b7623ebd84fa16f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Fri, 11 Aug 2023 23:23:37 +0200 Subject: [PATCH] Adapt w.r.t. coq/coq#17955. --- src/coq_elpi_builtins.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 4cc812479..2dcdbb699 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -2750,7 +2750,7 @@ Supported attributes:|} ^ hint_locality_doc))))), Coq_elpi_utils.detype env sigma |> Patternops.pattern_of_glob_constr) in let info = { Typeclasses.hint_priority; hint_pattern } in - Hints.add_hints ~locality [db] Hints.(Hints.HintsResolveEntry[info,true,PathHints [gr], hint_globref gr]); + Hints.add_hints ~locality [db] Hints.(Hints.HintsResolveEntry[info, true, hint_globref gr]); state, (), [] ))), DocAbove);