diff options
| author | Pierre-Marie Pédrot | 2019-11-29 17:50:34 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-11-29 17:50:34 +0100 |
| commit | 639886e771882e2c3302cbadc35e9383b34db1fe (patch) | |
| tree | b8939fb28c70c1fcdf9d953bffb2f289f2c6cf8b /tools | |
| parent | 37b1348d54df2d65389987e8bd920f9e1b275c44 (diff) | |
| parent | 686cf492c3bc8fcead400b45525d156c10ac3afb (diff) | |
Merge PR #11184: Undeprecate Add Setoid / Add Morphism.
Reviewed-by: ppedrot
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions