Stream: Coq users

Topic: Force notations to be Reserved


view this post on Zulip Ali Caglayan (Mar 24 2021 at 17:43):

Is it possible for coq to reject Notation commands unless it has been reserved beforehand?

view this post on Zulip Enrico Tassi (Mar 24 2021 at 17:48):

I don't think so. I'd like the same feature too (maybe a warning, to avoid breaking everything)


Last updated: Jan 28 2023 at 06:30 UTC