Mentions légales du service

Skip to content

Use OCaml dot notation for projections

HERBELIN Hugo requested to merge herbelin/itauto:master+adapt-coq-pr-17321-ocaml-dot-notation-for-projections into master

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.

Merge request reports