diff options
| author | Théo Zimmermann | 2019-11-26 11:18:35 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-11-26 11:18:35 +0100 |
| commit | 686cf492c3bc8fcead400b45525d156c10ac3afb (patch) | |
| tree | 333430dabc2cde95168768c2be90db8daf2615b8 /dev/include | |
| parent | 669075119cc0ea8e495a83668fad4f6c1e4f5968 (diff) | |
Undeprecate Add Setoid / Add Morphism.
The proposed replacements are not satisfying because they are more
complicated to use. Following the discussion in #8713, we decide to
remove the deprecation warning for these commands.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions