diff options
| author | Maxime Dénès | 2017-05-09 09:21:58 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-09 09:21:58 +0200 |
| commit | 8eb59a3f2551fd121fbc44dacf47818b6aeace03 (patch) | |
| tree | 30f220552ebbe556a503dc5387ba59f800d1f8b6 /dev/base_include | |
| parent | 98b6ccc4ffa2378e333961f9a59eb7ab0d174ee5 (diff) | |
| parent | 6532ee2d63c6e96b930895b0d42c8d9c7cc9e911 (diff) | |
Merge PR#621: Prevent user-defined ring morphisms from ever being evaluated.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions