diff options
| author | Maxime Dénès | 2019-05-16 18:20:07 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-06-06 08:54:39 +0200 |
| commit | fb30e8880a3027ef1c957df668a906d723e8a8a0 (patch) | |
| tree | ad2825c374340dfa0bb4c8785034e689c0311d61 /theories | |
| parent | c0a695e89b0562eb6450c04ddba5e6e0414e5fd8 (diff) | |
`deprecated` attribute support for notations and syntactic definitions
We also slightly change the semantics of the `compat` syntax modifier to
re-express it in terms of the `deprecated` attribute, and we deprecate
it in favor of the latter.
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Logic/Berardi.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v index 4576ff4cbe..bb4ed10bc9 100644 --- a/theories/Logic/Berardi.v +++ b/theories/Logic/Berardi.v @@ -149,6 +149,7 @@ apply AC_IF. Qed. -Notation classical_proof_irrelevence := classical_proof_irrelevance (compat "8.8"). +#[deprecated(since = "8.8", note = "Use classical_proof_irrelevance instead.")] +Notation classical_proof_irrelevence := classical_proof_irrelevance. End Berardis_paradox. |