Open
Description
Description of the problem
When explicitly passing the core hint database to auto tactics, the core database gets added twice to the list of dbs to use, resulting in the hints being tried twice. This is inefficient and probably not what the user wanted.
I think the whole core / nocore business is an unfortunate mess resulting from the lack of a proper API from the tactic world, but at least we should try to be consistent with the user intent.
Small Rocq / Coq file to reproduce the bug
Axiom foo : nat -> False.
Hint Resolve foo : core.
Goal False.
Proof.
debug auto.
(* debug auto: *)
(*
* assumption. (*fail*)
* intro. (*fail*)
* simple apply foo (in core). (*success*)
** assumption. (*fail*)
** intro. (*fail*)
*)
debug auto with core.
(*
(* debug auto: *)
* assumption. (*fail*)
* intro. (*fail*)
* simple apply foo (in core). (*success*)
** assumption. (*fail*)
** intro. (*fail*)
* simple apply foo (in core). (*success*)
** assumption. (*fail*)
** intro. (*fail*)
*)Version of Rocq / Coq where this bug occurs
No response
Interface of Rocq / Coq where this bug occurs
No response
Last version of Rocq / Coq where the bug did not occur
No response