The Coq mailing list

[Nicolas BERTAUX <nicolas.bertaux AT etu.upmc.fr>]

    Hello,

> Coq paths are made of iterated module field selections.  Having
> expressions like F(M) in paths would require computations at path
> resolution time. Coq could somehow hide a precomputation N of F(M) and
> reason with N in place of F(M) but this is not done. Hence, the user
> has to do the job of "precomputation" her/himself in advance.

    Thank you for your answer and your workaround. Do you plan to make this
feature more flexible in the future (typically, making those precomputations
done by Coq, for example)? In OCaml, applications can be used as effective
parameters of functors; could it be done in Coq in a similar way?

    Thanks again for your help.

    Nicolas.