diff options
| author | Michael Soegtrop | 2021-03-23 21:55:59 +0100 |
|---|---|---|
| committer | Michael Soegtrop | 2021-03-23 21:55:59 +0100 |
| commit | 47c20236f578dca9381822a62b5a406d6b42676d (patch) | |
| tree | fef686014dc1985799869ff1d6cab4e8f76ec8bc /plugins | |
| parent | fa2ba1571cbd791c3b1acd87adeacd0aa4bd6e88 (diff) | |
| parent | 83c11db006ca87b3912d2548593b669884a3b4b5 (diff) | |
Merge PR #13774: Allow to register deprecation status in Ltac2 term and notation declarations
Reviewed-by: JasonGross
Reviewed-by: Zimmi48
Ack-by: jfehrle
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions