diff options
| author | Pierre-Marie Pédrot | 2020-11-20 15:17:31 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-20 15:17:31 +0100 |
| commit | dac6017513cea37f96ce8256239e490f18339f08 (patch) | |
| tree | eae43761e97bdd403553182eec7afce51c3fa7a8 /interp/notation_ops.mli | |
| parent | 04186f83545e3c693976c73d488b36dd4a2b50db (diff) | |
| parent | f2a5096bf0829316eba869fe5d929337e6fd8bad (diff) | |
Merge PR #13399: Miscellaneous ring improvements in code + error messages
Reviewed-by: ppedrot
Diffstat (limited to 'interp/notation_ops.mli')
0 files changed, 0 insertions, 0 deletions