diff options
| author | Maxime Dénès | 2017-10-09 16:42:28 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-09 16:42:28 +0200 |
| commit | 5ef85c86dc94338c2d0da060946baafea2e5370e (patch) | |
| tree | 4e0ba603694a7bdea2771ca6f24eda549ce8ca5f /API | |
| parent | f927df44202034fa8cf73f72af876ae1e4ca05ba (diff) | |
| parent | 6526933e3d6a6392aa6bd5235ea0180bb68b6f94 (diff) | |
Merge PR #1126: [ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.
Diffstat (limited to 'API')
0 files changed, 0 insertions, 0 deletions