By uniformity, and to ensure awareness of what opacity is chosen, coq/coq#18795 proposes that opaque is now made a mandatory label of add_definition, like it is for other declaration functions of the API.
The label term is also renamed to body, again by consistency of naming.
By uniformity, and to ensure awareness of what opacity is chosen, coq/coq#18795 proposes that opaque is now made a mandatory label of
add_definition, like it is for other declaration functions of the API.The label
termis also renamed tobody, again by consistency of naming.To be merged synchronously with coq/coq#18795.