coq icon indicating copy to clipboard operation
coq copied to clipboard

Published 20 hours ago • verified publisher icon coq

Towards a single code path for the "using" clause + small improvement of "using Type" for co/fixpoints

Open herbelin opened this issue 1 year ago • 0 comments

The using clause was stored either in the Proof.t (for definitions generating proofs) or in the CInfo.t (for definitions with immediate proof, one for each component if a co/fixpoint). The PR makes a single choice by putting it instead in Info.t. In particular:

  • this addresses pending XXX comments in vernacentries.ml
  • this is a step towards having a single execution path for interactive and non-interactive Definition/Fixpoint (and eventually towards coq/ceps#42)

Note that we renounce to have one using per member of the CInfo.t on the assumption that the components of CInfo.t are mutually dependent, thus, having to share the same section variables (did I miss other uses of CInfo.t than for mutual definitions?).

In particular, we enhance a bit the effect of using Type on mutual definitions, taking all types together into account so that the dependencies are computed for the block of co/fixpoints as a whole.

@gares, @ejgallego: I believe it goes in the direction that you defended, I hope I'm not wrong.

  • [x] Added / updated test-suite.

herbelin avatar Mar 04 '24 08:03 herbelin