diff options
| author | Guillaume Melquiond | 2017-05-09 00:26:56 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2017-05-09 00:26:56 +0200 |
| commit | 6532ee2d63c6e96b930895b0d42c8d9c7cc9e911 (patch) | |
| tree | e94ddab092f2fc0ebdf837432001a35ede81a352 /dev/include | |
| parent | e5bf991cd1094ff1d5bc2f121bb6e85c8b1320c0 (diff) | |
Prevent user-defined ring morphisms from ever being evaluated.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions