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: Apr 20 2024 at 10:02 UTC