diff options
| author | Michael Soegtrop | 2020-05-10 08:45:19 +0200 |
|---|---|---|
| committer | Michael Soegtrop | 2020-05-10 08:45:19 +0200 |
| commit | d567eeeac238175e4d3d032f72a1409145abf89d (patch) | |
| tree | 1d8e5ec34fc06d4e522b09d2218ef27f11ad9b79 /interp/notation.mli | |
| parent | 2760d13b4bc70738cf10f1e6864764f62dcef32d (diff) | |
| parent | 598e24a9c4a81ec9f24f1088d0a7a4a93dc19fd4 (diff) | |
Merge PR #12287: Define CRzero and CRone via CR_of_Q
Reviewed-by: MSoegtropIMC
Diffstat (limited to 'interp/notation.mli')
0 files changed, 0 insertions, 0 deletions