Merge pull request #494 from ppedrot/hint-cut-static-globref

LPCIC · Sep 5, 2023 · 2aeae2e · 2aeae2e
2 parents a0d0eef + 5c23e96
commit 2aeae2e
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
@@ -2884,7 +2884,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);