Honor all registered modes when one mode is = - #22415

Honor all registered modes when one mode is =#22415

Janno wants to merge 1 commit into

rocq-prover:masterrocq-prover/rocq:masterfrom

Janno:janno/hint-mode-iJanno/coq:janno/hint-mode-iCopy head branch name to clipboard