Expose Section Variable Determining API in SerAPI about coq-serapi HOT 6 CLOSED

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?

from coq-serapi.

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]

from coq-serapi.

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

from coq-serapi.

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

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

from coq-serapi.

Demilestoning this until we have more feedback.

from coq-serapi.

Closing for now, happy to resurrect his if needed.

from coq-serapi.