Add warning about implicitly local HB.instance calls, improve error messages

[lweqx]

For more context, see the corresponding topic on Zulip.

Demo:

From HB Require Import structures.

HB.mixin Record Mixin T := {}.
HB.structure Definition _ := { T of Mixin T }.

HB.factory Record Factory T := {}.

HB.builders Context U of Factory U.

(* New warning:
  In builder mode, non-builder instances are always considered local.
  Annotate this HB.instance call with #[local] to fix this warning and improve your code documentation.
  [HB.nonlocal-instance-in-builder-mode,HB,elpi,default]
*)
HB.instance Definition _ := Mixin.Build unit.

(* Rocq error: HB: No builders on U to declare. This HB.builders section must HB.instance at least one mixin or factory on U.

  Previously: No builders to declare, did you forget HB.instance? 
*)
Fail HB.end.

(* Still ok *)
HB.instance Definition _ := Mixin.Build U.

(* Rocq error:
  HB: declare-instance: cannot make builders local. 
  If you want temporary instances, make an alias, e.g. with let U' := U

  Previously:
    HB: declare-instance: cannot make builders local.
        If you want temporary instances, make an alias, e.g. with let T' := T
*)
Fail #[local]
HB.instance Definition _ := Mixin.Build U.

HB.end.

[CohenCyril]

I'm also having second thoughts on whether to fail or warn on noop HB.end. indeed it is practical to be able to close a section without obstruction, in order to be able to evaluate further down in the file, an it is even more crucial when using Rocq lsp continuous mode since the rest of the file will be interpreted in the HB.builder context (despite the presence of HB.end) ...

[lweqx]

I think it should only be a warning mainly because writing code that does nothing is not an error. I don't think it really matters though.
I lack experience with Rocq LSP to really understand your comment about its continuous mode.

Happy to change it!