Adapt to coq/coq#19690 (Hint Extern respects default proof mode)#132

Draft

SkySkimmer wants to merge 1 commit intomit-plv:masterfrom SkySkimmer:ltacX-obligations

+2

Commits on Oct 15, 2024

Adapt to coq/coq#19690 (Hint Extern respects default proof mode)
SkySkimmer
committed