Expose Section Variable Determining API in SerAPI

[HazardousPeach]

The ML API has a mechanism to determine which section variables were used by a proof. Ideally, SerAPI would also allow this.

Emilio's comment on Zulip here: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Determining.20section.20variables.20used/near/365974818

[ejgallego]

As of 8.17 Coq can infer this information either by calling Proof_using.suggest_constant or by just referring to Declarations.const_hyps as done in About since 8.17.

I'm a bit unsure why the extra code for dep analysis in Proof_using is needed, @SkySkimmer , do you know why this is the case?

[SkySkimmer]

suggest generates a minimum expression for using const_hyps is the full list

So for instance

Section S.
Variable A : Type.
Variable a : A.
Variable b : A.

Goal A.
Proof.
exact a.
Qed.

suggest will say should start with Proof using a const_hyps will be [A; a]

[SkySkimmer]

Also suggest will give alternative builtin expressions when equivalent, so if we don't have variable b it will also suggest Type* and All.

[ejgallego]

Thanks @SkySkimmer , I hadn't understood what minimize meant in this context.

@HazardousPeach , I understand you want the const_hyps semantics here, right?

[ejgallego]

Demilestoning this until we have more feedback.

[ejgallego]

Closing for now, happy to resurrect his if needed.