towokit928 (Dec 29 2021 at 07:34): towokit928 (Dec 29 2021 at 07:34):Hi, I'm trying to compile a Coq project from 2017 with Coq 8.13.2 and am getting this error:
Error: fst is not a projection.
from code like this
st.(fst)
where st is value of a product type created with *.
I see a projection for fst defined here, so I'm not sure why this is happening. How can I allow this code to compile? In the same project, I see the same notation being used for a record defined with Record and it works.
Guillaume Melquiond (Dec 29 2021 at 07:41):Just replace the projection syntax by the function call syntax: fst st.
towokit928 (Dec 29 2021 at 08:04):That works, but that notation is used throughout the project. Is the projection syntax deprecated/reserved for records?
Guillaume Melquiond (Dec 29 2021 at 08:21):Yes; it is reserved for record projections.
towokit928 (Dec 29 2021 at 08:37):Thanks!
Notification Bot (Dec 29 2021 at 08:37):towokit928 has marked this topic as resolved.
Last updated: Oct 03 2023 at 20:01 UTC