Set Default Proof Using in sections survives the section end

[Blaisorblade]

Description of the problem

Section foo.
  Context`{Hinj : True}.
  Set Default Proof Using "Hinj".
End foo.

Lemma bar : True.
Fail Proof.
(* 
The command has indeed failed with message:
Unknown variable: Hinj
*)

Not a bug, and can be worked around via #[local] Set Default Proof Using "Hinj"., but seems surprising.

But for now I prefer the workaround — I've given up on remembering the default localities, especially since they started changing.

Coq Version

8.13.2

[Zimmi48]

One more argument in favor of making local the uniform default locality then... Except that in this case, it would become all the more important to be able to provide a local(module) attribute to emulate the current behavior.

[SkySkimmer]

Is it really that important? I'm not sure if anyone wants the current behaviour.

[Zimmi48]

I'm not sure if anyone wants the current behaviour.

Not sure either, but it's really important to have a foolproof compatibility solution (people could sprinkle #[ local(module) ] in front of all their Set / Unset commands for forward-compatibility, similarly to what they do today with #[ global ] in front of Hint commands).