Use OCaml dot notation for projections
Hi Frédéric, while working on bugs of extraction, I arrived to propose Coq PR #17341 which extends the pruning of unused inlined constants to modules (it was done only at toplevel before). As a consequence, since they are not used in the rest of the extracted code, the applicative form of projections (e.g. let elt x = x.elt
) might stop being extracted. However, the OCaml ppprover.ml
wrapper of itauto still refers to the applicative form (as e.g. in Annot.elt v
).
This PR replaces the applicative uses of Annot.elt
by their dot version (e.g. v.Annot.elt
) to anticipate Coq PR #17341.
I guess this will be fine to you. The alternative would be to ask explicitly Coq to extract the applicative form of Annot.elt
.
This is backwards compatible and can be merged as soon as now.