Simplifying the declaration of constants bound to primitive projections.

We factorize code from declareInd.ml and inductiveops.ml which was
already existing in record.ml.

We keep expansion of local definitions in the type of fields of
primitive records while these are not expanded in the non-primitive
case. This is to be consistent with what Indtypes.compute_projections
is doing. See discussion at #11135.

We keep the unused code from inductiveops.ml for possible future use
though.

Include improvements contributed by Gaëtan Gilbert.

0 files changed, 0 insertions, 0 deletions