diff options
| author | Hugo Herbelin | 2020-02-26 19:50:21 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-26 19:50:21 +0100 |
| commit | f97cb743386744e9da3ede4b6cf8c803c2f58fde (patch) | |
| tree | 587be188c84d33fcdac8cd72c029cfd2be7ac85a /interp/notation_ops.mli | |
| parent | 0e70be7868bdc500212631a956b01e94565cd2c3 (diff) | |
| parent | 0dab087b10598f79ffa4f907c6d93fb7932e1c5b (diff) | |
Merge PR #11644: Use implicit arguments in notations for eq.
Reviewed-by: herbelin
Diffstat (limited to 'interp/notation_ops.mli')
0 files changed, 0 insertions, 0 deletions