[declare] Consolidate Proof Using handling.

[ejgallego]

This is an old to-do from the times of declare.ml refactoring;
thanks to Hugo Herbelin for trying first with #18742 , which this PR
could replace.

We adopt the following convention:

• we remove the per-constant using field from CInfo.t (as in [Subsumed] Towards a single code path for the "using" clause + small improvement of "using Type" for co/fixpoints #18742)

• interactive commands pass their using attribute down to the proof
  initialization, where the parameter is interpreted properly in declare.ml

• ̶f̶o̶r̶ ̶n̶o̶w̶ ̶w̶e̶ ̶c̶h̶o̶o̶s̶e̶ ̶t̶o̶ ̶w̶a̶r̶n̶ ̶o̶n̶ ̶p̶l̶a̶c̶e̶s̶ ̶w̶h̶e̶r̶e̶ ̶u̶s̶i̶n̶g̶ ̶a̶t̶t̶r̶i̶b̶u̶t̶e̶s̶ ̶a̶r̶e̶ ̶n̶o̶t̶
  ̶ ̶ ̶u̶s̶e̶d̶ ̶(̶t̶r̶a̶n̶s̶p̶a̶r̶e̶n̶t̶ ̶d̶e̶f̶i̶n̶i̶t̶i̶o̶n̶ ̶n̶o̶t̶ ̶i̶n̶s̶i̶d̶e̶ ̶a̶ ̶s̶e̶c̶t̶i̶o̶n̶)̶

We add tests from #18742, written by Hugo.

cc: @herbelin

Overlays:

• [coq] Adapt to coq/coq#18890 coq-community/vscoq#767
• [coq] Adapt to coq/coq#18890 LPCIC/coq-elpi#628

[herbelin]

non-interactive commands ignore the using attribute (that could be resurrected maybe if we add an "Opaque" form)

add warning when attributes are not supported

Both the design choice of rejecting (as in the PR once the corresponding XXX are filled) or accepting (as in #13903) are ok to me. If it is e.g. easier for UI to reject, let's go this way.

[herbelin]

Good to me. There is the pending design decision of rejecting or accepting using on non-interative declarations.

[ejgallego]

Hi @herbelin , I tried to fix all the problems, this should be good to go now, modulo CI / unintended bugs.

[I was careful to review all the places that matter, and to preserve the behavior, but still there is margin for errors]

[ejgallego]

@herbelin actually there are some tests that fail now due to this:

Section T.
Variables (T : Type) (x : T).
#[using="x"] Definition test : unit := tt.
End test.
Check test : forall T, T -> unit.

So indeed maybe we want to restore the use of the attribute in this case, right?

That would be easy to do, I guess we could also warn when the attribute is passed but no sections are opened.

[herbelin]

So indeed maybe we want to restore the use of the attribute in this case, right?

I don't have a strong opinion, but this kinds of feature for immediate definitions is not a problem for UIs, I would preserve the ability to do it.

[ejgallego]

Hi @herbelin , sorry for the wait, I rebased this PR, and I hope I can do the remaining changes before the weekend.

[ejgallego]

@herbelin this should be ready, a few comments:

• I've removed the warning entirely, as it was quite confusing together with the error when using is used outside sections. I suggest improvements on user display to happen in a different PR
• There are some possible minor improvements still to do in the code, but I think this is a good checkpoint

[herbelin]

• warning entirely, as it was quite confusing together with the error when using is used outside sections. I suggest improvements on user display to happen in a different PR

• There are some possible minor improvements still to do in the code, but I think this is a good checkpoint

OK to me. (I just added a comment about solve_obligations but it can be in another PR too).

So, I'm assigning and, unless told differently, I'm going to merge this awaited old to-do when the CI is checked.

[ejgallego]

OK to me. (I just added a comment about solve_obligations but it can be in another PR too).

Thanks a lot @herbelin ; I think indeed we need to handle what is going on there, but I suggest I do so in a different PR as to allow depending PRs to move independently.

[herbelin]

@coqbot merge now

[coqbot-app]

@herbelin: Please take care of the following overlays:

• 18890-ejgallego-no_using_cinfo.sh